Browse Teach Curate

Primal-Dual Framework for Program Verification Algorithms via Generalized Lagrangians

Generalizes the Lagrangian of linear programming to the discrete domains of verification (powersets of states, predicates, ranking functions) so that a Lagrangian induces a primal and a dual problem; an abstract procedure searches both simultaneously with monotonicity conditions that guarantee progress, unifying algorithms such as CEGAR, ICE learning and lazy SMT as instances and yielding a new validity checker for fixpoint logic over quantified linear arithmetic.

Demerzel Text

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

This paper builds a single primal-dual framework that unifies many program-analysis, verification, and automated-reasoning algorithms whose common structure is a simultaneous search for a proof and f…