[12-23] latticed k-induction with an application to probabilistic programs
文章来源： | 发布时间：2022-12-12 | 【】 【】
title:latticed k-induction with an application to probabilistic programs
speaker:mingshuai chen (rwth aachen university)
time:12月23日（周五）上午10:00-12:00
venue:线下：5号楼三层334报告厅；线上：腾讯会议 327-136-793
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
