Termination and Invariance Analysis of Loops

Abstract

Deductive verification aims to prove deep properties about programs. The classic Floyd-Hoare-style approach to verifying sequential programs reduces program validity queries to first-order validity queries via verification conditions. Proving that a program is totally correct requires proving the safety aspect with invariants and the progress aspect with invariants and ranking functions. Where do the invariants and ranking functions come from?

A verifying compiler that reads program annotations enables the programmer to write desired properties as assertions. Unfortunately, verifying a safety property requires strengthening it to an inductive assertion, while proving termination requires finding ranking functions. The strengthening process often involves writing many tedious facts, while ranking functions are not always intuitive. In practice, programmers do not want or are unable to invent inductive assertions and ranking functions. Instead, the ideal verifying compiler strengthens the given assertions with facts learned through static analysis. Invariant generators are a class of static analyzers that automatically synthesize inductive invariants. Ranking function generators automatically synthesize ranking functions, sometimes with supporting invariants. Together, they reduce the burden on the programmer by automatically learning facts about programs.

In this talk, we discuss our approach to invariant and ranking function generation. A constraint-based method labels program points with parameterized expressions, which encode the shape of the desired inductive assertions or ranking functions. For example, the shape of an inductive invariant could be an inequality between affine combinations of program variables, while the shape of a ranking function could be an affine combination of program variables. It then generates a set of parameterized verification conditions and solves for the parameter values that make them valid. Instantiating the parameterized expressions with these values results in a set of inductive assertions or ranking functions. We discuss recent work for analyzing termination of programs that manipulate variables via affine expressions. We also discuss a constraint-based analysis for programs with integer division and modulo operators. Finally, we present experimental evidence indicating that invariant and ranking function generation is a powerful technique for scaling deductive verification to large programs.