软件形式化方法、符号计算、信息安全技术

   

081203-计算机应用技术

软件形式化验证
符号计算
信息安全技术

2003-09--2009-07   中国科学院成都计算所   工学博士

   

2012-02~现在, 中国科学院重庆绿色智能技术研究院, 副研究员
2009-07~2012-02,电子科技大学, 讲师

   

（1） 团队突出贡献奖, , 研究所（学校）, 2005

（ 1 ） 一类有界闭连通域上的循环程序终止性判断方法, 发明, 2015, 第 1 作者, 专利号: 2015101811056
（ 2 ） 一种用于符号线性系统的快速高斯约当消去方法, 发明, 2015, 第 1 作者, 专利号: 201510362146.5

   

（1） Detecting multiphase linear ranking functions for single-path linear-constraint loops, INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2021, 通讯作者
（2） SVMRanker: A General Termination Analysis Framework of Loop Programs via SVM., ESEC/FSE2020, 2020, 第 1 作者
（3） On ranking functions for single-path linear-constraint loops, INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2020, 通讯作者
（4） 多项式循环程序的秩函数探测, Detection of Ranking Functions of Polynomial Loop Programs, 软件学报, 2019, 第 1 作者
（5） 基于SVM的多项式循环程序秩函数探测, 软件学报, 2019, 第 1 作者
（6） Ranking Function Detection via SVM: A More General Method, IEEE ACCESS, 2019, 通讯作者
（7） Synthesizing Nested Ranking Functions for Loop Programs via SVM, ICFEM2019, 2019, 第 1 作者
（8） Parameterized inequalities about a point in the plane of a triangle, JOURNAL OF MATHEMATICAL INEQUALITIES, 2018, 第 2 作者
（9） 基于k阶秩函数的线性赋值循环程序的终止性分析, Termination Analysis of Linear Assignment Loop Program Based on k-ranking Functions, 计算机科学, 2018, 第 1 作者
（10） A Sufficient Criterion for Termination of Multi-path Linear Assignment Loops, EMBEDDED SYSTEMS TECHNOLOGY, ESTC 2017, 2018, 通讯作者
（11） Termination of semi-algebraic loop programs, SETTA2017, 2017, 第 1 作者
（12） 计算最终线性秩函数的新方法, New Method for Computing Eventual Linear Ranking Functions, 计算机科学, 2017, 第 2 作者
（13） Witness to non-termination of linear programs, THEORETICAL COMPUTER SCIENCE, 2017, 通讯作者
（14） The L-depth Eventual Linear Ranking Functions for Single-path Linear Constraint Loops, 2016 10TH INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE), 2016, 通讯作者
（15） Eventual Linear Ranking Functions for Multi-path Linear Loops, 2016 IEEE INFORMATION TECHNOLOGY, NETWORKING, ELECTRONIC AND AUTOMATION CONTROL CONFERENCE (ITNEC), 2016, 通讯作者
（16） 有界闭连通域上的非线性循环终止性分析, Termination Analysis of Non-Linear Loops over Closed and Bounded Connected Domain, 软件学报, 2016, 第 1 作者
（17） Termination of Single-Path Polynomial Loop Programs, THEORETICAL ASPECTS OF COMPUTING - ICTAC 2016, 2016, 通讯作者
（18） Termination of Initialized Two Variable Homogeneous Linear Loops, ICSESS, 2015, 第 1 作者
（19） 多分支单变量循环程序的终止性分析, Termination Analysis of Multipath Loop Programs with One Variable, 软件学报, 2015, 第 1 作者
（20） Termination Analysis of Programs with Periodic Orbit on the Boundary, ISRME, 2015, 第 1 作者
（21） A recursive decision method for termination of linear programs, 2014 Symposium on Symbolic-Numeric Computation, SNC 2014, 2014, 第 1 作者
（22） 一类带初始输入的线性循环终止性分析, Termination Analysis of a Class of Initialized Linear Loops, 四川大学学报：工程科学版, 2014, 第 2 作者
（23） 有界闭域上的线性赋值循环终止性分析, Termination Analysis of Loops with Linear Assignment over Closed and Bounded Domains, 软件学报, 2014, 第 1 作者
（24） 基于完全判别系统的程序终止性证明, ISISE’12, 2013, 第 1 作者
（25） 线性循环程序的终止性判定, 系统科学与数学, 2013, 第 1 作者
（26） 非线性循环的终止性分析, Termination Analysis of Nonlinear Loops, 软件学报, 2012, 第 1 作者
（27） Proving Program Termnation by Discoverer and Complete Discrimination System, ISISE, 2012, 第 1 作者
（28） Automatic synthesis of multiple ranking functions with supporting invariants via DISCOVERER, Proc. of the 3rd International Conference on Advanced Computer Theory and Engineering, 2010, 第 1 作者
（29） Termination of Programs over the Union of Intervals, ICACIT’10, 2010, 第 1 作者
（30） 有理单变元表示在最优化问题上的应用, 系统科学与数学, 2009, 第 1 作者
（31） 一类循环条件非线性的程序终止性, Termination of a Class of Nonlinear Loop Programs, 四川大学学报：工程科学版, 2009, 第 2 作者
（32） Automatic Discovery of Non-Linear Ranking Functions of Loop Programs, 2009 2ND IEEE INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE AND INFORMATION TECHNOLOGY, VOL 1, 2009, 通讯作者
（33） 线性程序的Ranking函数自动合成, Automatic Synthesis of Linear Program Ranking Functions, 四川大学学报：工程科学版, 2009, 第 2 作者
（34） An effective hybrid algorithm for computing symbolic determinants, APPLIED MATHEMATICS AND COMPUTATION, 2009, 通讯作者
（35） 一类半正定多项式的配平方和算法, AN ALGORITHM FOR SUMS OF SQUARES OF A CLASS OF POSITIVE SEMI-DEFINITE POLYNOMIALS, 系统科学与数学, 2008, 第 1 作者
（36） An effective algorithm of computing symbolic determinants with multivariate polynomial entries, APPLIED MATHEMATICS AND COMPUTATION, 2007, 通讯作者
（37） 基于降维的并行符号行列式计算, An Algorithm of Computing Symbolic Determinants Based on Dimension -decreasing, 四川大学学报：工程科学版, 2007, 第 1 作者

   

（ 1 ） 软件正确性分析的自动推理方法及工具的开发, 负责人, 地方任务, 2012-07--2015-08
（ 2 ） 陆地交通混成系统安全性分析与验证, 参与, 中国科学院计划, 2013-01--2015-12
（ 3 ） 微分代数方程中的误差可控计算理论与算法, 参与, 国家任务, 2015-01--2018-12
（ 4 ） 零误差计算理论与应用, 参与, 中国科学院计划, 2014-06--2016-12
（ 5 ） 多项式循环程序的终止性研究及其应用, 负责人, 国家任务, 2016-01--2019-12
（ 6 ） 几类While循环终止性分析的理论、方法及其应用, 负责人, 国家任务, 2012-01--2014-12
（ 7 ） 参数半代数系统的误差可控计算理论与算法, 参与, 国家任务, 2018-01--2021-12
（ 8 ） 基于计算机代数的代码终止性分析方法研究, 负责人, 地方任务, 2019-08--2022-07
（ 9 ） 基于格密码的轻量级同态加密理论与应用, 参与, 地方任务, 2019-12--2022-12
（ 10 ） 灵动公交算法研究, 负责人, 企业委托, 2021-03--2021-12