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. 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.
Short bio:
Mingshuai Chen is currently a postdoctoral researcher at the Chair for Software Modeling and Verification, Department of Computer Science, RWTH Aachen University, Aachen, Germany. He received his Ph.D. degree in computer science from the Institute of Software, Chinese Academy of Sciences, Beijing, China in 2019. His research interest lies in the general scope of formal verification and synthesis, broadly construed in mathematical logic and theoretical computer science. In particular, he is interested in formal reasoning of programs and hybrid discrete-continuous systems, for ensuring the reliability and effectiveness of safety-critical cyber-physical systems, and aims to push the limits of automation as far as possible. Mingshuai Chen 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; he has co-authored around 20 peer-reviewed papers spanning the areas of formal methods, computer-aided verification, control synthesis, and automated reasoning, which have been published at top-tier journals/conferences including IEEE Trans. Automat. Contr., Acta Informatica, CAV, TACAS, FM, IJCAR, and CADE.
腾讯会议 ID：117 728 939
会议链接：https://meeting.tencent.com/dm/Wwv6KEx9L8Z5
