|
我的研究领域为程序理论、软件形式化方法、信息物理融合系统，近年来的工作主要包括：
- 协调模型和语言的设计及相关工具开发：Reo与Mediator，
- 深度学习系统、信息物理融合系统、安全攸关系统、量子系统、概率并发系统、随机实时系统、安全协议、区块链智能合约等复杂系统的正确性、安全性、可信性保障技术与方法，
- 余代数理论、余归纳推理方法及其在复杂系统建模与验证中的应用，
- 模型检验、定理证明、约束求解等形式化验证技术，
- 机器学习与深度学习系统的理论基础及相关技术在形式化验证中的应用，
- 基于模型的软件测试、代码分析与自动生成，
- 面向服务与云计算。
如果你想了解更多，或加入我的课题组，欢迎和我联系。
部分在研项目：
- 2022-2025，深度学习系统的可信性保障（项目主持人，国家自然科学基金面上）
- 2022-2025，双层一体安全高性能区块链智能合约语言关键技术研究（课题负责人，国家重点研发计划）
部分已完成项目：
- 2022-2023，基于Mediator的面向协议建模语言设计及工具实现（项目主持人，CCF-华为胡杨林基金）
- 2021-2022，大规模深度学习系统形式化建模与验证（项目主持人，CCF-华为胡杨林基金）
- 2019-2021，高可信深度学习：理论与技术（课题负责人，广东省重点领域研发项目）
- 2018-2021，信息物理系统中复杂并发行为的形式化建模与验证（项目主持人，国家自然科学基金面上）
- 2019-2020，移动应用大数据分析（项目主持人，企业合作）
- 2016-2020，大规模概率并发实时系统的模型检验（主要成员，国家自然科学基金重点）
- 2018-2019，智能合约安全性建模与验证（项目主持人，企业合作）
- 2017-2018，公安行业大数据挖掘（项目主持人，企业合作）
- 2015-2018，随机和混成系统验证中的可组合性、抽象化方法和带参问题的研究（主要成员，中德合作）
- 2013-2016，面向对象程序的分离逻辑理论基础（主要成员，国家自然科学基金面上）
- 2013-2015，基于Reo的协调理论及其在信息物理系统开发方法中的应用（项目主持人，国家自然科学基金青年基金）
- 2013-2015，基于Reo的实时及混成连接件建模与验证方法（项目主持人，教育部博士点基金）
- 2011-2012，构件化软件的QoS验证及测试方法研究（项目主持人，中国科学院软件研究所开放课题）
- 2006-2010，Coordination with Performance Guarantees （主要成员，荷兰NWO）
- 2005-2007，余代数及其在软件方法学中的应用（主要成员，国家自然科学基金面上）
- 2004，第10届代数方法与软件技术国际会议（项目主持人，国家自然科学基金国际合作与交流项目）
- 2003-2005，基于组件程序设计的形式化基础（主要成员，科技部中葡合作）
- Decision-Guided Weighted Automata Extraction from Recurrent Neural Networks. in Proceedings of AAAI 2021, pages 11699-11707, 2021. (CCF A, joint work with Xiyue Zhang, Xiaoning Du, Xiaofei Xie, Lei Ma and Yang Liu)
- Mediator: A Component-based Modeling Language for Concurrent and Distributed Systems. Science of Computer Programming, vol. 192, 2020. (CCF B, joint work with Yi Li and Weidi Sun)
- Characterizing Adversarial Defects of Deep Learning Software from the Lens of Uncertainty. in Proceedings of ICSE 2020, pages 739-751, ACM, 2020. (CCF A, joint work with Xiyue Zhang, Xiaofei Xie, Lei Ma, Xiaoning Du, Qiang Hu, Yang Liu and Jianjun Zhao)
- A Formal Framework Capturing Real-Time and Stochastic Behavior in Connectors. Science of Computer Programming，vol. 177, pages 21-40, 2019. (CCF B, joint work with Yi Li, Xiyue Zhang, Yuanyi Ji. This is an extended version of the SBMF 2017 paper, which got the Best Paper Award at the conference.)
- A Formal Specification and Verification Framework for Timed Security Protocols. in IEEE Transactions on Software Engineering, vol. 44(8), pages 725-746, 2018. (CCF A, joint work with Li Li, Jun Sun, Yang Liu and Jinsong Dong)
- CCF形式化方法专委战略研讨会，2024.5.5，苏州：深度神经网络的语义鲁棒性
- 西北工业大学，2023.12.12: Mediator-based Protocol Modeling and Verification
- 粤港澳大湾区数字经济研究院，2023.12.11: All the Scenes on Earth Fade——When Blockchain Embraces Formal Verification
- 同济大学，2023.12.4：All the Scenes on Earth Fade——When Blockchain Embraces Formal Verification
- 华东师范大学，2023.12.4: Mediator-based Protocol Modeling and Verification
- CCF中国软件大会2023高可信嵌入式软件智能化开发与测试论坛邀请报告，2023.12.1，上海：深度神经网络的语义鲁棒性
- LEDS 2023可信软件工程中的逻辑方法研讨会邀请报告，2023.11.3-5，喀什：基于Mediator的协议建模与验证
- CNCC 2023云网融合中的网络形式化方法前沿技术论坛邀请报告, 2023.10.27，沈阳：当区块链遇上形式化验证
- Invited talk at Huawei Hong Kong Formal Methods Workshop, 2023.8.22: What Will Happen When AI Embraces Formal Methods?
- 东南大学，2023.5.20：All the Scenes on Earth Fade——When Blockchain Embraces Formal Verification
- CCF中国软件大会2022人工智能安全论坛邀请报告，2022.11，上海（线上）：强化学习系统的变异测试
- CCF中国软件大会2022华为胡杨林基金论坛报告， 2022.11，上海（线上）：基于Mediator的面向协议建模语言设计及工具实现
- CISAM 2022年会区块链理论技术及应用挑战论坛报告，2022.11，清远（线上）：基于区块链的供应链金融设计模式
- Invited talk at AILA 2022，2022.8，上海（线上报告）: A Unifying Logic for Neural Networks
- 中国计算机学会形式化⽅法专委“可信AI”专题学术研讨会，2022.4：⼤规模深度学习系统形式化建模与验证
- 中国工业与应用数学学会金融科技与算法专委会首届年会报告，2022.1，珠海（线上报告）：All the Scenes on Earth Fade——When Blockchain Embraces Formal Verification
- CCF Chinasoft 2021 talk，2021.12，北京: Formal Modeling and Verification of Large-Scale Deep Learning Systems
- CSIAM 2021 annual conference talk，2021.10，合肥: Modeling and Verification of CKB Consensus Protocol in Coq
- Invited talk at CSIAM-BTAF 2021， 2021.7，苏州，All the Scenes on Earth Fade——When Blockchain Embraces Formal Verification
- Invited talk at Beijing-Saint Petersburg Mathematics Colloquium, 2020.12: Modeling and Verification of Concurrent and Distributed Systems: From Reo to Mediator
- 华为首届ICT软件技术大会特邀报告, 2020.10, 西安: 现代数学发展对软件的启发与应用
- 国防科技大学, 2020.10: Modeling and Verification of Concurrent and Distributed Systems: From Reo to Mediator
- Invited talk at FROM 2020: Modeling and Verification of Concurrent and Distributed Systems in Mediator
- FinTech Public Course, 2020.8：Towards Safe FinTech: When Blockchain Meets Formal Verification
- 首都师范大学信息工程学院, 2019: Modeling and Verifying Complex Interactions in Concurrent Systems
- Invited talk at AI&FM'19: Using RNN to Predict Tactics for Theorem Proving
- Invited talk at CSIAM 2019 annual conference: Towards a Formally Verified EVM
- 华东师范大学, 2019.11: Using RNN to Predict Tactics for Theorem Proving
- Invited Speaker at FMSES 2018: Using Coq and Recurrent Neural Network to Model and Verify Connectors
- Panelist: YOSER 2017, Beijing
- 中国计算机学会（CCF）形式化方法专业委员会执行委员（2016-）
- 中国计算机学会（CCF）区块链专业委员会执行委员（2023-）
- 中国工业与应用数学学会（CSIAM）金融科技与算法专业委员会常务委员（2022-）
- 中国工业与应用数学学会（CSIAM）区块链专业委员会委员（2020-2023），常务委员（2023-）
- 中国人工智能学会（CAAI）人工智能逻辑专业委员会委员（2023-）
- Associate Editor: Frontiers in Computer Science (Section Theoretical Computer Science, 2021.3-)
- Journal Editorial Board Member: Frontiers in Computer Science (2019-2021), Frontiers in ICT (2015-2019) and Frontiers in Applied Mathematics and Statistics (2015-2018)
- PC member, FSEN 2025, Västerås, Sweden, April, 2025
- PC Co-chair, ICFEM 2024, Hiroshima, Japan, December, 2024
- PC member (形式化方法与应用论坛), CCF ChinaSoft 2024, Xi'an, China, November, 2024
- PC member, ICTAC 2024, Bangkok, Thailand, November, 2024
- PC member, SEFM 2024, Aveiro, Portugal, November, 2024
- PC member, SEKE 2024, Amalfi, Italy, October, 2024
- PC Co-chair, FACS 2024, Milan, Italy, September, 2024 (co-locate with FM 2024)
- PC member, ICSI 2024, Xining, China, August, 2024
- PC Co-chair, CSIAM区块链专委会2024年会, 长春, June, 2024
- PC member, Coordination 2024, Groningen, the Netherlands, June, 2024
- PC member, ICECCS 2024, Limassol, Cyprus, June, 2024
- PC member, FMBC 2024, Luxembourg, April, 2024
- PC member (形式化方法与应用论坛), CCF ChinaSoft 2023, Shanghai, China, December, 2023
- PC member, SETTA 2023, Nanjing, China, November, 2023
- PC member, DSAI 2023, Bangkok, Thailand, November, 2023
- PC member, ICFEM 2023, Brisbane, Australia, November, 2023
- PC member, LEDS 2023, Kashi, China, November, 2023
- PC member, BSC 2023, Chiang Mai, Thailand, October, 2023
- PC member, FACS 2023, Virtually, October, 2023
- SC member, AILA 2023, Changchun, China, August, 2023
- PC Co-chair, TASE 2023, Bristol, UK, July, 2023
- PC member, ICSI 2023, Shenzhen, China, July, 2023
- PC member, SEKE 2023, San Francisco Bay, USA, July, 2023
- PC member, Coordination 2023, Lisbon, Portugal, June, 2023
- PC member, ICECCS 2023, Toulouse, France, June, 2023
- PC member, 2023区块链技术与应用高峰论坛, 海口, May, 2023
- PC member, FSEN 2023, Tehran, Iran, May, 2023
- PC member, 2023粤港澳大湾区人工智能、区块链与金融科技国际会议, 珠海, April, 2023
- PC member, BSC 2022, Guangzhou, China, December, 2022
- PC member (约束求解与定理证明论坛), CCF ChinaSoft 2022, Shanghai, China, November, 2022
- PC member, SETTA 2022, Beijing, China, October, 2022
- PC member, ICFEM 2022, Madrid, Spain, October, 2022
- PC member, FMBC 2022, Haifa, Israel, August, 2022
- PC member, TASE 2022, Cluj, Romania, July, 2022
- PC member, SEKE 2022, San Francisco Bay, USA, July, 2022
- PC member, LCA 2022, Aveiro, Portugal, June, 2022
- PC member, Coordination 2022, Lucca, Italy, June, 2022
- PC member, ICECCS 2022, Hiroshima, Japan, March, 2022
- Track Chair (形式化方法与应用论坛) and PC member (定理证明理论与应用论坛): CCF ChinaSoft 2021, Xi'an, China, November, 2021
- PC member: MEMOCODE'21, Virtual, November, 2021
- PC member: FM 2021 Doctoral Symposium, Virtual, November, 2021
- PC member: SETTA'21, Beijing, China, November, 2021
- Publicity Chair: ATVA'21, Gold Coast, Australia, October, 2021
- PC Co-chair: MLiSE 2021, Virtual, September, 2021
- PC member: TASE'21, Shanghai, China, August, 2021
- PC member: FMBC'21, Los Angeles, USA, July, 2021
- PC member: SEKE'21, San Francisco Bay, USA, July, 2021
- PC member: Coordination'21, Valletta, Malta, June, 2021
- PC member: FSEN'21, Tehran, Iran, May, 2021
- Track Chair（形式化方法教育论坛）and PC member: CCF ChinaSoft 2020, Chongqing, China, November, 2020
- Local Organization Chair and PC member: SETTA'20, Guangzhou, China, November, 2020
- PC member: KEOD'20, Budapest, Hungary, November, 2020
- PC member: ICFEM'20, Singapore, November, 2020 (postponed to March, 2021 due to COVID-19)
- PC member: ICECCS'20, Singapore, October, 2020 (postponed to March, 2021 due to COVID-19)
- PC member: GAUSS'20, Coimbra, Portugal, October, 2020
- PC member: SEFM'20, Amsterdam, the Netherlands, September, 2020
- PC member: FOCLASA'20, Amsterdam, the Netherlands, September, 2020
- PC member: ASYDE'20, Amsterdam, the Netherlands, September, 2020
- PC member: QEST'20, Vienna, Austria, August-September, 2020
- Track Chair: IJTCS'20, Beijing, China, August, 2020
- PC member: FMBC'20, Los Angeles, USA, July, 2020
- PC member: TASE'20, Hangzhou, China, July, 2020
- PC member: SEKE'20, Pittsburgh, USA, July, 2020
- PC member: Coordination'20, Valletta, Malta, June, 2020
- PC member: FormaliSE'20, Seoul, Korea, May, 2020
- PC member: FMAC'19, Shanghai, China, November, 2019
- PC member: ICECCS'19, Hong Kong, China, November, 2019
- PC member: ICFEM'19, Shenzhen, China, November, 2019
- PC member: AI&FM'19, Shenzhen, China, November, 2019
- PC member: NASAC'19 (SYSCONSTRCUT Track), Hangzhou, China, November, 2019
- PC member: GAUSS'19, Berlin, Germany, October, 2019
- PC member: FM'19, Porto, Portugal, October, 2019
- PC member: FOCLASA'19, Oslo, Norway, September, 2019
- PC member: ASYDE'19, Oslo, Norway, September, 2019
- PC member: TASE'19, Guilin, China, July, 2019
- PC member: SEKE'19, Lisbon, Portugal, June, 2019
- PC member: Coordination'19, Lyngby, Denmark, June, 2019
- PC member: FSEN'19, Tehran, Iran, May, 2019
- PC member: TACAS'19, Prague, Czech Republic, April, 2019
- PC member: MLCSB'18, Santiago, Chile, December, 2018
- PC Co-chair: ICFEM'18, Gold Coast, Australia, November, 2018
- PC member: SDLT'18, Gold Coast, Australia, November, 2018
- PC member: FMAC'18, Chongqing, China, November, 2018
- PC member: YR-FMAC'18, Chongqing, China, November, 2018
- PC member: FACS'18, Pohang, Korea, October, 2018
- PC member: FORMATS'18, Beijing, China, September, 2018
- Publicity Chair: CONCUR'18, Beijing, China, September, 2018
- Organizer: CAP 2018, Beijing, China, September, 2018
- PC member: SEKE'18, San Francisco, USA, July, 2018
- PC member: FOCLASA'18, Toulouse, France, June, 2018
- PC member: YR-SETTA'17, Changsha, China, October, 2017
- PC member: FMAC'17, Changsha, China, October, 2017
- PC member: FACS'17, Braga, Portugal, October, 2017
- Organization Co-Chair, MAVeLoS'17, Beijing, China, October, 2017
- PC member: EGOSE'17, St. Petersburg, Russia,September, 2017
- PC member: FOCLASA'17, Trento, Italy, September, 2017
- Organizer: CAP 2017, Heidelberg, Germany, July, 2017
- PC member: SEKE'17, Pittsburgh, USA, July, 2017
- PC member: FSEN'17, Tehran, Iran, April, 2017
- Organizer: PKU Forum on Theoretical Frontiers of Information Science, Beijing, China, November, 2016
- PC member: EGOSE'16, St. Petersburg, Russia, November, 2016.
- PC member: FMAC'16, Beijing, China, November, 2016
- PC member: YR-SETTA'16, Beijing, China, November, 2016
- PC member: DTGS'16, St. Petersburg, Russia, June, 2016
- PC member: Coordination'16, Heraklion, Greece, June, 2016
- PC member: UTP'16, Reykjavik, Iceland, June, 2016
- PC member: YR-SETTA'15, Nanjing, China, November, 2015
- PC member: FOCLASA'15, Madrid, Spain, September, 2015
- PC member: FM 2015 Doctoral Symposium, Oslo, Norway, June, 2015
- PC member: FSEN'15, Tehran, Iran, April, 2015
- PC member: FOCLASA'14, Rome, Italy, September, 2014
- PC member: FACS'14, Bertinoro, Italy, September, 2014
- PC member: UTP'14, Singapore, May, 2014
- PC member & Publicity Chair: FACS'13, Nanchang, China, October, 2013
- PC member: FSEN'13, Tehran, Iran, April, 2013
- PC member: FACS'12, Mountain VIew, USA, September, 2012
- PC member: UTP'12, Paris, France, August, 2012
- PC member: TASE'12, Beijing, China, July, 2012
- PC member: Coordination'12,
Stockholm, Sweden, June, 2012
- PC member: UML&FM 2012, Paris, France, July, 2012
- PC member: UML&AADL 2012, Paris, France, July, 2012
- PC Co-chair: TTSS'11, Oslo, Norway, September, 2011
- PC member and SC member: FACS'11, Oslo, Norway, September, 2011
- PC member: ICFEM'11, Durham, UK, October, 2011
- PC member: Coordination'11,
Reykjavik, Iceland, June, 2011
- PC member & Publicity Chair: UML&AADL
2011, Las Vegas, USA, April, 2011
- PC member: UML&FM 2011, Lero, Limerick, Ireland, June, 2011
- PC member: FSEN'11, Tehran, Iran,
April, 2011
- PC member: UTP'10,
Shanghai, China, November, 2010
- PC member: TTSS'10,
Shanghai, China, November, 2010
- PC member & Publicity Chair: UML&FM 2010, Shanghai, China, November, 2010
- PC member and SC member: FACS'10,
Guimaraes, Portugal, October, 2010
- PC member & Publicity Chair: UML&AADL
2010, Oxford, UK, March, 2010
- Organization Chair of the SYANCO
winter school, Berlin, Germany, February, 2010
- PC Co-Chair and SC member: FACS'09,
Eindhoven, the Netherlands, November, 2009
- PC member & Publicity Chair: UML&FM
2009, Rio de Janeiro, Brasil, December, 2009
- PC member & Publicity Chair: UML&AADL
2009, Potsdam, Germany, June, 2009
- PC member: FCST'09,
Shanghai, China, October, 2009
- PC member: TTSS'08,
Nanjing, China, June, 2008
- PC member: TTSS'07,
Macau, China, September, 2007
- Publicity Chair: TASE'07,
Shanghai, China, June 2007
- PC member: FACS'06,
Prague, Czech Republic, September, 2006
- PC member: FACS'05,
Macau, China, October, 2005
- 会议论文评审:
ICFEM'02, ICFEM'03, FACS'03, SEFM'05, ICTAC'05, ICFEM'05, LOPSTR'05,
ICDCIT'05, ICSE'06, SAC'06(Track SV), FSEN'07, ICTAC'07, FM'08,
Coordination'08, AMAST'08, SBLP'08, WS-FM'08, HASE'08, SAC'09(Track CM),
FSEN'09, ICFEM'09, SBMF'12, ICTAC'14, ICTAC'16, FM'16, Chinasoft'22 (Track FMAC), SETSS 2024
- 期刊论文评审(2024): ACM Transactions on Software Engineering and Methodology，软件学报，计算机工程与科学，智能安全
- 期刊论文评审(2023): ACM Transactions on Software Engineering and Methodology, IEEE Transactions on Software Engineering, Journal of Logical and Algebraic Methods in Programming, Journal of Systems Architecture, 软件学报，智能安全，华东师范大学学报
- 期刊论文评审(2022): Science of Computer Programming, Formal Aspects of Computing, Journal of Systems Architecture, Journal of Logical and Algebraic Methods in Programming, 软件学报，智能安全
- 期刊论文评审(2021): ACM Transactions on Software Engineering and Methodology, IEEE Transactions on Software Engineering, Theoretical Computer Science, Formal Aspects of Computing, Journal of Computer Science and Technology, Frontiers of Information Technology & Electronic Engineering, Innovations in Systems and Software Engineering, 中国科学, 软件学报
- 期刊论文评审(2020): Formal Aspects of Computing, Science of Computer Programming, International Journal on Software Tools for Technology Transfer, Journal of Computer Science and Technology, Frontiers of Computer Science, Frontiers of Information Technology & Electronic Engineering, Internatioanl Journal on Software Engineering and Knowledge Engineering, Microprocessors and Microsystems
- 期刊论文评审(2019 and before):
ACM Transactions on Software Engineering and Methodology, IEEE Transactions on Reliability, Internatioanl Journal on Software Engineering and Knowledge Engineering, Software and System Modeling, Formal Aspects of Computing, Journal of Logical and Algebraic Methods in Programming, Theoretical Computer Science, Science of Computer Programming, Theoretical Informatics and Applications, Fundamenta Informaticae, International Journal of Computer
Systems Science and Engineering, 中国科学，软件学报，华南理工大学学报.
