Constraint solving for program verification: Theory and practice by example

Abstract. Program verification relies on the construction of auxiliary assertions describing various aspects of program behaviour, e.g., in-ductive invariants, resource bounds, and interpolants for characterizing reachable program states, ranking functions for approximating number of execution steps until program termination, or recurrence sets for demon-strating non-termination. Recent advances in the development of con-straint solving tools offer an unprecedented opportunity for the efficient automation of this task. This paper presents a series of examples illustrat-ing algorithms for the automatic construction of such auxiliary assertions by utilizing constraint solvers as the basic computing machinery.