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:2025m Research paper | Software Model-Checking as Cyclic-Proof SearchRemote POPLDOI Media Attached | ||
| 10:4525m 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 UniversityDOI Media Attached | ||
| 11:1025m 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 WaterlooDOI Media Attached | ||
| 11:3525m 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 SciencesDOI Media Attached | ||

