Mon 16 Jan 2023 09:00 - 10:00 at Arlington - Keynote and contribution paper Chair(s): Michael Emmi

Inferring inductive invariants is one of the main challenges of formal verification. One of the latest breakthroughs in invariant inference is property-directed reachability (IC3/PDR). In this talk we investigate some of the unique properties of propositional PDR from the theoretical perspective. First, we show that the SAT queries performed by PDR, which enable an incremental construction of the invariant, are more powerful than simple inductiveness checks. In particular, we show that IC3 cannot be implemented in the ICE framework. Second, we utilize the rich theory of abstract interpretation to shed light on the overapproximation of the reachable states performed by PDR’s frames. Namely, we define an eager version of PDR, called Lambda-PDR, in which all generalizations of counterexamples are used to strengthen a frame, and show that its frames can be formulated as an abstract interpretation algorithm in a logical domain based on Bshouty’s monotone theory. Since the frames of Lambda-PDR are tighter than the frames of PDR, the same overapproximation, and more, is present in PDR’s frames. We demonstrate that this overapproximation can result in an exponential gap compared to exact forward reachability.

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
Keynote and contribution paper VMCAI at Arlington
Chair(s): Michael Emmi Amazon Web Services
Towards a Theoretical Understanding of Property-Directed Reachability
Sharon Shoham Tel Aviv University
Distributing and Parallelizing Non-canonical Loops
Clément Aubert Augusta University, Thomas Rubiano LIPN – UMR 7030 Université Sorbonne Paris Nord, Neea Rusch Augusta University, Thomas Seiller CNRS