Wed 19 Jan 2022 10:45 - 11:10 at Salon I - Automated Verification Chair(s): Roberto Giacobazzi

Many invariant inference techniques reason simultaneously about states and predicates, and it is well-known that these two kinds of reasoning are in some sense dual to each other. We present a new formal duality between states and predicates, and use it to derive a new primal-dual invariant inference algorithm. The new induction duality is based on a notion of provability by incremental induction that is formally dual to reachability, and the duality is surprisingly symmetric. The symmetry allows us to derive the dual of the well-known Houdini algorithm, and by combining Houdini with its dual image we obtain primal-dual Houdini, the first truly primal-dual invariant inference algorithm. An early prototype of primal-dual Houdini for the domain of distributed protocol verification can handle difficult benchmarks from the literature.

Wed 19 Jan

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

10:20 - 12:00
Automated VerificationPOPL at Salon I
Chair(s): Roberto Giacobazzi University of Verona
10:20
25m
Research paper
Software Model-Checking as Cyclic-Proof SearchRemote
POPL
Takeshi Tsukada Chiba University, Hiroshi Unno University of Tsukuba; RIKEN AIP
DOI Media Attached
10:45
25m
Research paper
Induction Duality: Primal-Dual Search for InvariantsRemote
POPL
Oded Padon VMware Research; Stanford University, James R. Wilcox Certora, Jason R. Koenig Stanford University, Kenneth L. McMillan University of Texas at Austin, Alex Aiken Stanford University
DOI Media Attached
11:10
25m
Research paper
Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive FunctionsRemote
POPL
Hari Govind V K University of Waterloo, Sharon Shoham Tel Aviv University, Arie Gurfinkel University of Waterloo
DOI Media Attached
11:35
25m
Research paper
Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and VariablesRemote
POPL
Taolue Chen Birkbeck University of London, Alejandro Flores Lamas Royal Holloway University of London, Matthew Hague Royal Holloway University of London, Zhilei Han Tsinghua University, Denghang Hu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Shuanglong Kan TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer Uppsala University, Zhilin Wu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences
DOI Media Attached