083500-软件工程

形式化方法

2009-10--2014-05   法国格勒诺布尔大学   博士
2007-09--2009-09   法国国立航空航天学院   硕士
2002-09--2006-09   中国民航大学   学士

   

2018-03~2023-02,深圳大学, 副研究员
2014-07~2018-02,清华大学, 博士后
2009-10~2014-05,法国格勒诺布尔大学, 博士
2007-09~2009-09,法国国立航空航天学院, 硕士
2002-09~2006-09,中国民航大学, 学士

   

（1） Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks, ACM Transactions on Software Engineering and Methodology, 2024, 第 3 作者  通讯作者
（2） 基于K Framework的向量化机器学习指令语义形式化, Semantics Formalization of Vectorized Machine Learning Instructions in K Framework, 软件学报, 2023, 
（3） COQCRYPTOLINE: A Verified Model Checker with Certified Results, CAV, 2023, 第 4 作者
（4） llvm2CryptoLine:VerifyingArithmeticinCryptographicC Programs, FSE, 2023, 第 3 作者
（5） Certified Verification for Algebraic Abstraction, CAV, 2023, 第 4 作者
（6） MpBP: verifying robustness of neural networks with multi-path bound propagation, FSE, 2022, 第 3 作者
（7） Verified NTT Multiplications for NISTPQC KEM Lattice Finalists: Kyber, SABER, and NTRU, TRANSACTIONS ON CRYPTOGRAPHIC HARDWARE AND EMBEDDED SYSTEMS, 2022, 第 4 作者
（8） 基于多路径回溯的神经网络验证方法, Multi-path Back-propagation Method for Neural Network Verification, 软件学报, 2022, 
（9） CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver, CAV, 2021, 第 1 作者
（10） Verifying Arithmetic in Cryptographic C Programs, 34TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2019), 2019, 
（11） Signed Cryptographic Program Verification with Typed CRYPTOLINE, PROCEEDINGS OF THE 2019 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'19), 2019, 
（12） Towards Verified Faithful Simulation, DEPENDABLE SOFTWARE ENGINEERING: THEORIES, TOOLS, AND APPLICATIONS, SETTA 2015, 2015, 

   

（ 1 ） 机载程序多重浮点精度向量运算正确性形式验证, 负责人, 地方任务, 2022-01--2024-12
（ 2 ） 飞控程序中多重精度运算正确性形式化验证, 负责人, 地方任务, 2021-10--2024-10
（ 3 ） 密集计算程序可配置混合精度浮点数向量运算的形式化验证, 负责人, 国家任务, 2021-01--2023-12