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.

@article{paperbot1538,
  title = {Induction duality: primal-dual search for invariants},
  author = {Oded Padon and James R. Wilcox and Jason R. Koenig and Kenneth L. McMillan and Alex Aiken},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {6},
  number = {POPL},
  year = {2022},
  doi = {10.1145/3498712}
}