An Interface Theory for Program Verification

Abstract

Program verification is the problem, for a given program and a specification of constructing a proof of correctness for the statement “program satisfies specification or a proof of violation (). Usually, a correctness proof is based on inductive invariants, and a violation proof on a violating program trace. Verification engineers typically expect that a verification tool exports these proof artifacts. We propose to view the task of program verification as constructing a behavioral interface (represented e.g. by an automaton). We start with the interface of the program itself, which represents all traces of program executions. To prove correctness, we try to construct a more abstract interface of the program (overapproximation) that satisfies the specification. This interface, if found, represents more traces than that are all correct (satisfying the specification). Ultimately, we want a compact representation of the program behavior as a correctness interface in terms of inductive invariants. We can then extract a correctness witness, in standard exchange format, out of such a correctness interface. Symmetrically, to prove violation, we try to construct a more concrete interface of the program (underapproximation) that violates the specification. This interface, if found, represents fewer traces than that are all feasible (can be executed). Ultimately, we want a compact representation of the program behavior as a violation interface in terms of a violating program trace. We can then extract a violation witness, in standard exchange format, out of such a violation interface. This viewpoint exposes the duality of these two tasks — proving correctness and violation. It enables the decomposition of the verification process, and its tools, into (at least!) three components: interface synthesizers, refinement checkers, and specification checkers. We hope the reader finds this viewpoint useful, although the underlying ideas are not novel. We see it as a framework towards modular program verification.