招生专业 083500-软件工程 081202-计算机软件与理论

招生方向 形式化方法

教育背景 2010-09--2014-06 普林斯顿大学 博士学位 2007-09--2010-06 麻省理工学院 学士学位 工作简历 2017-08~2018-07,慕尼黑工业大学, 博士后 2014-09~2017-06,麻省理工学院, 博士后 数理逻辑和程序理论 程序理论部分：2019-2020秋季、2020-2021秋季。 科研项目 （ 1 ） ****C类, 主持, 部委级, 2019-01--2020-12

形式化方法、交互式定理证明、嵌入式系统建模和验证。

（1） Learning One-Clock Timed Automata, Tools and Algorithms for the Construction and Analysis of Systems, 2020, 第 3 作者 （2） Design of Point-and-Click User Interfaces for Proof Assistants, Formal Methods and Software Engineering, 2019, 通讯作者 （3） Smooth manifolds and types to sets for linear algebra in Isabelle/HOL, International Conference on Certified Programs and Proofs, 2019, 第 2 作者 （4） Formal verification of quantum algorithms using quantum Hoare logic, International Conference on Computer Aided Verification, 2019, 通讯作者 （5） NIL: Learning Nonlinear Interpolants, International Conference on Automated Deduction, 2019, 通讯作者 （6） Efficient Verification of Imperative Programs Using Auto2, Tools and Algorithms for the Construction and Analysis of Systems, 2018, 第 1 作者 （7） Verifying Asymptotic Time Complexity of Imperative Programs in Isabelle, International Joint Conference on Automated Reasoning, 2018, 第 1 作者 （8） Formalization of the Fundamental Group in Untyped Set Theory Using Auto2, Interactive Theorem Proving, 2017, 第 1 作者 （9） Auto2, A Saturation-Based Heuristic Prover for Higher-Order Logic, Interactive Theorem Proving, 2016, 第 1 作者