The papers “Latticed k-Induction with an Application to Probabilistic Programs” by Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja and Philipp Schröer and “Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming” by Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan and Joost-Pieter Katoen have both been accepted as regular papers for CAV 2021.

The first paper revisits k-induction and bounded model checking (BMC) in the general setting of fixed point theory over complete lattices and shows that both generalised techniques can be used for the fully automatic verification of infinite-state probabilistic programs.

The second paper presents a new (weaker) condition on barrier certificates for hybrid systems that can attain inductive invariance and shows that discharging the barrier-certificate condition can be encoded as an optimization problem subject to bilinear matrix inequalities.