Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)

Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham

TL;DR

This work addresses the lack of a unified formal basis for duality-based verification algorithms by introducing a generalized Lagrangian L: X × Y → P that maps discrete verification domains into a totally ordered lattice. It then defines a primal-dual search procedure that simultaneously refines primal and dual candidates, guaranteeing progress under monotonicity assumptions and enabling a common lens to view diverse techniques such as CEGAR, ICE, and Houdini. The authors demonstrate that these algorithms are instances of the framework and derive a new primal-dual method for solving formulas in fixpoint logic over quantified linear arithmetic, accompanied by a prototype with promising results. By examining termination and robustness through strong/weak duality and stratification, the framework clarifies why certain methods converge or diverge and provides a blueprint for designing new verification tools that blend refinement, induction, and strategy synthesis.

Abstract

Many algorithms in verification and automated reasoning leverage some form of duality between proofs and refutations or counterexamples. In most cases, duality is only used as an intuition that helps in understanding the algorithms and is not formalized. In other cases, duality is used explicitly, but in a specially tailored way that does not generalize to other problems. In this paper we propose a unified primal-dual framework for designing verification algorithms that leverage duality. To that end, we generalize the concept of a Lagrangian that is commonly used in linear programming and optimization to capture the domains considered in verification problems, which are usually discrete, e.g., powersets of states, predicates, ranking functions, etc. A Lagrangian then induces a primal problem and a dual problem. We devise an abstract primal-dual procedure that simultaneously searches for a primal solution and a dual solution, where the two searches guide each other. We provide sufficient conditions that ensure that the procedure makes progress under certain monotonicity assumptions on the Lagrangian. We show that many existing algorithms in program analysis, verification, and automated reasoning can be derived from our algorithmic framework with a suitable choice of Lagrangian. The Lagrangian-based formulation sheds new light on various characteristics of these algorithms, such as the ingredients they use to ensure monotonicity and guarantee progress. We further use our framework to develop a new validity checking algorithm for fixpoint logic over quantified linear arithmetic. Our prototype achieves promising results and in some cases solves instances that are not solved by state-of-the-art techniques.

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)

TL;DR

This work addresses the lack of a unified formal basis for duality-based verification algorithms by introducing a generalized Lagrangian L: X × Y → P that maps discrete verification domains into a totally ordered lattice. It then defines a primal-dual search procedure that simultaneously refines primal and dual candidates, guaranteeing progress under monotonicity assumptions and enabling a common lens to view diverse techniques such as CEGAR, ICE, and Houdini. The authors demonstrate that these algorithms are instances of the framework and derive a new primal-dual method for solving formulas in fixpoint logic over quantified linear arithmetic, accompanied by a prototype with promising results. By examining termination and robustness through strong/weak duality and stratification, the framework clarifies why certain methods converge or diverge and provides a blueprint for designing new verification tools that blend refinement, induction, and strategy synthesis.

Abstract

Many algorithms in verification and automated reasoning leverage some form of duality between proofs and refutations or counterexamples. In most cases, duality is only used as an intuition that helps in understanding the algorithms and is not formalized. In other cases, duality is used explicitly, but in a specially tailored way that does not generalize to other problems. In this paper we propose a unified primal-dual framework for designing verification algorithms that leverage duality. To that end, we generalize the concept of a Lagrangian that is commonly used in linear programming and optimization to capture the domains considered in verification problems, which are usually discrete, e.g., powersets of states, predicates, ranking functions, etc. A Lagrangian then induces a primal problem and a dual problem. We devise an abstract primal-dual procedure that simultaneously searches for a primal solution and a dual solution, where the two searches guide each other. We provide sufficient conditions that ensure that the procedure makes progress under certain monotonicity assumptions on the Lagrangian. We show that many existing algorithms in program analysis, verification, and automated reasoning can be derived from our algorithmic framework with a suitable choice of Lagrangian. The Lagrangian-based formulation sheds new light on various characteristics of these algorithms, such as the ingredients they use to ensure monotonicity and guarantee progress. We further use our framework to develop a new validity checking algorithm for fixpoint logic over quantified linear arithmetic. Our prototype achieves promising results and in some cases solves instances that are not solved by state-of-the-art techniques.
Paper Structure (28 sections, 22 theorems, 55 equations, 2 figures, 4 algorithms)

This paper contains 28 sections, 22 theorems, 55 equations, 2 figures, 4 algorithms.

Table of Contents

  1. Introduction
  2. Lagrange Duality for Linear Programming and Verification
  3. Duality in Linear Programming
  4. Generalized Lagrange Duality
  5. A Primal-Dual Procedure
  6. Lagrangians for Safety Verification: CEGAR and ICE
  7. Problem setting
  8. Lagrangian for CEGAR
  9. Lagrangian for ICE
  10. Lagrangian for Primal-Dual Houdini
  11. Warmup: CEGAR for Cartesian Abstraction
  12. Induction Duality
  13. Lagrangian for Primal-Dual Houdini
  14. A More Abstract View
  15. Lagrangians for Termination Verification
  16. ...and 13 more sections

Key Result

lemma 1

Every Lagrangian $L \colon X \times Y \longrightarrow P$ enjoys the weak duality:

Figures (2)

  • Figure 1:
  • Figure : Primal-Dual Procedure

Theorems & Definitions (33)

  • definition 1: Lagrangian
  • definition 2
  • lemma 1
  • Remark 1
  • Remark 2
  • theorem 3
  • theorem 4
  • theorem 5
  • theorem 6
  • theorem 7
  • ...and 23 more