| Abstract: |
I revisit two well-established verification techniques, k-induction and bounded model checking (BMC), in the more general setting of fixed point theory over complete lattices. The main theoretical contribution is latticed k-induction, which (i) generalizes classical k-induction for verifying transition systems, (ii) generalizes Park induction for bounding fixed points of monotonic maps on complete lattices, and (iii) extends from naturals k to transfinite ordinals κ, thus yielding κ-induction (pronounced “kappa induction”). The lattice-theoretic understanding of k-induction and BMC enables us to apply both techniques to the fully automatic verification of infinite-state probabilistic programs. Our prototypical implementation manages to automatically verify non-trivial specifications for probabilistic programs taken from the literature that — using existing techniques — cannot be verified without synthesizing a stronger inductive invariant first. |
| Bio: |
Mingshuai Chen is currently a Postdoctoral Researcher at the Chair for Software Modeling and Verification, RWTH Aachen University, Aachen, Germany. He will soon join Zhejiang University, Hangzhou, China as a Young Professor leading the Formal Verification Group <https://fiction-zju.github.io/>. He received the Ph.D. degree in computer science from the Institute of Software, Chinese Academy of Sciences, Beijing, China in 2019. His primary research interest lies in formal verification and synthesis, broadly construed in mathematical logic and theoretical computer science. In particular, he develops 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. Mingshuai Chen has co-authored over twenty peer-reviewed papers at flagship journals/conferences including Inf. Compt., IEEE Trans. Automat. Contr., CAV, TACAS, IJGAR, FM etc.; he is the awardee of the Distinguished Paper Award at ATVA 2018, the Best Paper Award at FMAC 2019, and the CAS-President Special Award in 2019. |
