Induction Duality: Primal-Dual Search for InvariantsRemote
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 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00 | |||
10:20 25mResearch paper | Software Model-Checking as Cyclic-Proof SearchRemote POPL DOI Media Attached | ||
10:45 25mResearch 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 25mResearch 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 25mResearch 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 |