Mingshuai Chen

Mingshuai Chen

ZJU100 Young Professor

Zhejiang University

I am a US-equivalent tenure-track Assistant Professor leading the Formal Verification Group at Zhejiang University. Prior to joining ZJU, I worked as a Postdoctoral Researcher at the Software Modeling and Verification Group headed by Prof. Joost-Pieter Katoen at RWTH Aachen University. In 2019, I received the Ph.D. degree in computer science from the Institute of Software, Chinese Academy of Sciences under the supervision of Prof. Naijun Zhan and co-supervision of Prof. Martin Fränzle.

My primary research interest lies in formal verification and synthesis, broadly construed in mathematical logic and theoretical computer science. I develop formal reasoning techniques for programs and hybrid discrete-continuous systems for ensuring the reliability and effectiveness of safety-critical software systems while pushing the limits of automation as far as possible. I appreciate – and have been constantly fascinated by – the elegance of mathematical aspects of computer science as well as its impact on real-world applications. See the research statement for my faculty application at ZJU.

Check out my CV for more detailed information.

Interests

  • Formal Methods
  • Logic · Verification · Synthesis
  • Quantitative Reasoning
  • Programming Theory/Languages
  • Probabilistic/Quantum Systems
  • Cyber-Physical Systems

Education

  • Ph.D. in Computer Science, 2019

    Institute of Software, Chinese Academy of Sciences

  • B.Sc. in Computer Science, 2013

    Jilin University

Publications

Dissertation

  1. (2019). Verification and Synthesis of Time-Delayed Dynamical Systems. Cite Slides CAS-President Special Award

Book Chapters

  1. (2024). A Unified Framework for Quantitative Analysis of Probabilistic Programs. JPK’s Festschrift. PDF Cite DOI
  2. (2017). MARS: A Toolchain for Modelling, Analysis and Verification of Hybrid Systems. ProCoS. PDF Cite Code DOI

Journal Articles

  1. (2024). A Privacy Policy Text Compliance Reasoning Framework with Large Language Models for Healthcare Services. Tsinghua Sci. Tech.. PDF Cite
  2. (2024). Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions. Proc. ACM Program. Lang. (OOPSLA). PDF Cite Artifact Evaluated
  3. (2023). Lower Bounds for Possibly Divergent Probabilistic Programs. Proc. ACM Program. Lang. (OOPSLA). PDF Cite Poster Slides DOI
  4. (2022). Encoding Inductive Invariants as Barrier Certificates. Inf. Comput.. PDF Cite Code Slides DOI
  5. (2020). From Model to Implementation: A Network Algorithm Programming Language. Sci. China Inf. Sci.. PDF Cite Code DOI
  6. (2020). Indecision and Delays are the Parents of Failure. Acta Inform.. PDF Cite Code Slides Video DOI
  7. (2019). In Memory of Oded Maler: Automatic Reachability Analysis of Hybrid-State Automata. ACM SIGLOG News. PDF Cite DOI
  8. (2018). Reachability Analysis for Solvable Dynamical Systems. IEEE Trans. Automat. Contr.. PDF Cite Code DOI

Conference Papers

  1. (2024). UniGM: Unifying Multiple Pre-trained Graph Models via Adaptive Knowledge Aggregation. In ACM MM 2024. PDF Cite Code DOI
  2. (2024). Parf: Adaptive Parameter Refining for Abstract Interpretation. In ASE 2024. PDF Cite Code DOI
  3. (2024). Proving Functional Program Equivalence via Directed Lemma Synthesis. In FM 2024. PDF Cite
  4. (2024). Horae: A Domain-Agnostic Modeling Language for Automating Multimodal Service Regulation. In ICWS (SRG) 2024. PDF Cite
  5. (2024). MorphQPV: Exploiting Isomorphism in Quantum Programs to Facilitate Confident Verification. In ASPLOS 2024. PDF Cite Code DOI Artifact Evaluated
  6. (2024). QuFEM: Fast and Accurate Quantum Readout Calibration Using the Finite Element Method. In ASPLOS 2024. PDF Cite Code DOI
  7. (2024). Latticed Craig Interpolation with an Application to Probabilistic Verification. In CIBD 2024. PDF Cite
  8. (2023). Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants. In TACAS 2023. PDF Cite DOI Artifact Evaluated
  9. (2023). Exact Probabilistic Inference Using Generating Functions. In LAFI 2023. PDF Cite Code
  10. (2022). Does a Program Yield the Right Distribution?. In CAV 2022. PDF Cite DOI Artifact Evaluated
  11. (2021). Latticed $k$-Induction with an Application to Probabilistic Programs. In CAV 2021. PDF Cite Slides DOI Artifact Evaluated Pulp Fiction
  12. (2021). Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming. In CAV 2021. PDF Cite Slides Video DOI Artifact Evaluated
  13. (2020). Unbounded-Time Safety Verification of Stochastic Differential Dynamics. In CAV 2020. PDF Cite Slides Video DOI Artifact Evaluated Pulp Fiction
  14. (2020). Learning One-Clock Timed Automata. In TACAS 2020. PDF Cite Slides DOI Artifact Evaluated Best Paper Award @ FMAC 2019 Springer High-Impact Paper
  15. (2019). NIL: Learning Nonlinear Interpolants. In CADE 2019. PDF Cite Code Slides DOI
  16. (2019). Taming Delays in Dynamical Systems. In CAV 2019. PDF Cite Slides DOI Artifact Evaluated
  17. (2018). What's to Come is Still Unsure. In ATVA 2018. PDF Cite Code Slides Video DOI Distinguished Paper Award
  18. (2017). Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations. In FORMATS 2017. PDF Cite Slides Video DOI
  19. (2017). A Two-Way Path between Formal and Informal Design of Embedded Systems. In UTP 2016. PDF Cite Code Slides DOI
  20. (2016). Validated Simulation-Based Verification of Delayed Differential Dynamics. In FM 2016. PDF Cite Code Poster Slides DOI
  21. (2016). Computing Reachable Sets of Linear Vector Fields Revisited. In ECC 2016. PDF Cite Code Slides DOI
  22. (2016). Interpolant Synthesis for Quadratic Polynomial Inequalities and Combination with EUF. In IJCAR 2016. PDF Cite Code Slides DOI
  23. (2015). Decidability of the Reachability for a Family of Linear Vector Fields. In ATVA 2015. PDF Cite Code Slides DOI

Preprints

  1. (2024). Horae: A Domain-Agnostic Modeling Language for Automating Multimodal Service Regulation. arXiv. Preprint. PDF Cite Code Dataset
  2. (2022). PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot. arXiv. Preprint. PDF Cite DOI
  3. (2020). On Termination of Polynomial Programs with Equality Conditions. arXiv. Preprint. PDF Cite Code DOI