工作经历
2017-2019 信息科学系 主任
2008-2017 北京大学数学科学学院 副院长
2000- 北京大学数学科学学院 讲师、副教授、教授
1998-2000 北京大学数学系 博士后
2008-2017 北京大学数学科学学院 副院长
2000- 北京大学数学科学学院 讲师、副教授、教授
1998-2000 北京大学数学系 博士后
代表作
1. L. Yang, X. Hou and B. Xia, A complete algorithm for automated discovering of a class of inequality-type theorems, Science in China, Series F, Vol. 44, No. 1, pp.33--49, 2001.
2. B. Xia and L. Yang, An algorithm for isolating the real solutions of semi-algebraic systems, J. of Symbolic Computation, Vol. 34, No.5, pp.461--477, 2002.
3. L. Yang and B. Xia: Real solution classifications of a class of parametric semi-algebraic systems. In: Algorithmic Algebra and Logic --- Proceedings of the A3L 2005 (A. Dolzmann, A. Seidl, and T. Sturm, eds.), pp. 281—289. Herstellung und Verlag, Norderstedt (2005).
4. B. Xia: DISCOVERER: A tool for solving semi-algebraic systems, Software Demo at ISSAC 2007, Waterloo, July 30, 2007. Also: ACM SIGSAM Bulletin, Vol. 41, No. 3, pp.102--103, Sept., 2007.
5. B. Xia and L. Yang: Automated Inequality Proving and Discovering. World Scientific, 344 pages, Aug. 2016.
2. B. Xia and L. Yang, An algorithm for isolating the real solutions of semi-algebraic systems, J. of Symbolic Computation, Vol. 34, No.5, pp.461--477, 2002.
3. L. Yang and B. Xia: Real solution classifications of a class of parametric semi-algebraic systems. In: Algorithmic Algebra and Logic --- Proceedings of the A3L 2005 (A. Dolzmann, A. Seidl, and T. Sturm, eds.), pp. 281—289. Herstellung und Verlag, Norderstedt (2005).
4. B. Xia: DISCOVERER: A tool for solving semi-algebraic systems, Software Demo at ISSAC 2007, Waterloo, July 30, 2007. Also: ACM SIGSAM Bulletin, Vol. 41, No. 3, pp.102--103, Sept., 2007.
5. B. Xia and L. Yang: Automated Inequality Proving and Discovering. World Scientific, 344 pages, Aug. 2016.
科研项目
1、面向程序验证的自动定理证明理论、方法与工具研究（项目批准号 61732001），国家自然科学基金重点项目
2、大规模概率并发实时系统模型检验（项目批准号 61532019），国家自然科学基金重点项目
3、复杂曲面流线场的保向共轭理论与线性化方法 (项目批准号 11290141), 国家自然科学基金重大项目 "基于流线场共轭映射的复杂曲面高精度数控加工新方法"
4、半代数系统的高效求解算法及其在不等式机器证明中的应用，国家自然科学基金面上项目
5、混成系统设计与验证中的符号计算方法和工具，中科院软件所开放课题
6、代数系统的准确可信计算，国家自然科学基金 国际合作与交流项目
7、基于计算机代数的我国高速列车运行控制系统规范CTCS-3/4的分析与验证, 国家自然科学基金重大研究计划“可信软件基础研究”培育项目
8、基于计算机代数的嵌入式软件分析与验证方法及工具（重点项目），国家自然科学基金 重大研究计划
9、新世纪优秀人才支持计划 （NCET），教育部
10、Chinese-SALSA，法国INRIA研究所国际合作项目
11、实代数符号计算在形式化方法中的应用，国家自然科学基金面上项目
12、海量信息系统协同性随机模型与可生存性复杂性分析，国家973项目：海量信息的协同性和可生存性的理论与实践研究
13、实几何与实代数的高效能算法，国家973项目：数学机械化方法及其在信息领域中的应用
14、自动推理平台，国家973项目：数学机械化与自动推理平台
2、大规模概率并发实时系统模型检验（项目批准号 61532019），国家自然科学基金重点项目
3、复杂曲面流线场的保向共轭理论与线性化方法 (项目批准号 11290141), 国家自然科学基金重大项目 "基于流线场共轭映射的复杂曲面高精度数控加工新方法"
4、半代数系统的高效求解算法及其在不等式机器证明中的应用，国家自然科学基金面上项目
5、混成系统设计与验证中的符号计算方法和工具，中科院软件所开放课题
6、代数系统的准确可信计算，国家自然科学基金 国际合作与交流项目
7、基于计算机代数的我国高速列车运行控制系统规范CTCS-3/4的分析与验证, 国家自然科学基金重大研究计划“可信软件基础研究”培育项目
8、基于计算机代数的嵌入式软件分析与验证方法及工具（重点项目），国家自然科学基金 重大研究计划
9、新世纪优秀人才支持计划 （NCET），教育部
10、Chinese-SALSA，法国INRIA研究所国际合作项目
11、实代数符号计算在形式化方法中的应用，国家自然科学基金面上项目
12、海量信息系统协同性随机模型与可生存性复杂性分析，国家973项目：海量信息的协同性和可生存性的理论与实践研究
13、实几何与实代数的高效能算法，国家973项目：数学机械化方法及其在信息领域中的应用
14、自动推理平台，国家973项目：数学机械化与自动推理平台
主讲课程
每学期 符号计算与程序验证讨论班 研究生
秋季 理论计算机科学基础 本科生、研究生
春季 符号计算 研究生、本科生
2019春季 3+X 讨论班 本科生
2020秋季 3+X 讨论班 本科生
秋季 理论计算机科学基础 本科生、研究生
春季 符号计算 研究生、本科生
2019春季 3+X 讨论班 本科生
2020秋季 3+X 讨论班 本科生
社会兼职
1、中国工业与应用数学会常务理事
2、中国数学会计算机数学专委会副主任
3、中国计算机学会形式化方法专业组委员
4、国际学术期刊 Mathematics in Computer Science 编委
5、《系统科学与数学》第八届编委
6、北京智源人工智能研究院“人工智能的数理基础”重大研究方向项目经理
7、十届海淀区政协常委
8、九三学社北京市委委员、九三学社北京大学委员会副主委
2、中国数学会计算机数学专委会副主任
3、中国计算机学会形式化方法专业组委员
4、国际学术期刊 Mathematics in Computer Science 编委
5、《系统科学与数学》第八届编委
6、北京智源人工智能研究院“人工智能的数理基础”重大研究方向项目经理
7、十届海淀区政协常委
8、九三学社北京市委委员、九三学社北京大学委员会副主委
荣誉获奖
2020年 北京大学教学优秀奖
2005-2006年度 北京大学教学优秀奖
2001年 周培源数学奖教金
2000-2001 年度优秀班主任
2005-2006年度 北京大学教学优秀奖
2001年 周培源数学奖教金
2000-2001 年度优秀班主任