课程：
符号计算（研究生+本科生），每周三下午7-9节，三教407。
讨论班：
本学期北大符号计算讨论班：周四下午3-5点
本学期软件所程序验证联合讨论班：周五上午10-12点
指导的学生：
在读博士生：赵天琪，吴雨伦，陈日增，倪新鹏，李夏鲲，王凯章。
出站博士后：王杰 （2019年6月）
已毕业的研究生：张颋（2004届），陈长波（2006届），陈应华（2007届），田雷（2007届），刘昆（2008届），马蕾（2009届），肖溶（2010届春季博士），方天（2010届） ，张志海（2011届博士），李颖麟（2011届），沈非（2012届），钱笑羽（2013届），唐晓弦（2014届博士） ，代立云（2015届春季博士），陈正鸿（2015届博士），张怡（2016届） ，甘庭（2017届春季博士），张瀚文（2018届） ，范哲（2019届），冯怡珺（2019届博士），王宇（2019届博士） ，于欣彤（2020届） ，郑涛（2021届博士）， 张慧颖（2021届），赵舸航（2021届），李昊坤（2022届博士），周括（2022届），于奕清（2023届）
本科生（校长基金）：丁剑、汪腾（2002级），姚珧（2003级），赵琳博（2004级），谭昌汇（2004级），韩京俊、金陟（2009级）
本科生（国家大学生创新训练计划）：王轩、殷小平（2005级元培），秦腾（2007级）