Automated Deductive Translation of Guardol Programs and Specifications into SMT-Provable Properties

Presented as part of the 2013 HCSS conference.

The verification architecture of the Guardol system uses an implementation of HOL (Higher Order Logic) as a front end to SMT (Satisfiability Modulo Theories) technology. SMT provides high levels of proof automation. HOL provides semantic power, modelling the operational semantics of Guardol, an imperative language, and justifying the automatic deductive translation of programs to the functional form needed by SMT technology. In the Guardol system, extensive manipulation of programs and specifications is performed in HOL before goals are sent to the backend RADA SMT system. The pervasive use of deductive transformations means that such manipulations preserve meaning up until the backend SMT system is invoked, giving the final proof results a high level of assurance.
We focus the discussion on three topics: induction, arrays, and partiality.

1. Since Guardol supports guards over tree-structured data, inductive proofs need to be automated. We show how this is aided by the derivation of induction schemes for recursive programs, and illustrate how the initial segment of an inductive proof is carried out on the HOL side before the invocation of RADA.
2. Arrays are an interesting class of types, sitting in between recursive structures and finite types: although arrays are finite, operations on arrays are implemented as a recurrence, often via loop constructs. We have focused on supporting FOR-loops: these are naturally modelled by tail-recursion, or (equivalently) a WHILE construct, both of which are difficult to reason about. However, we have formulated a simple and general theorem, capturing folklore workarounds in a single rewrite rule, that transforms such tail recursions into primitive recursions, which are easier to reason about. In the Guardol verification architecture, this transformation is applied by rewriting before any induction takes place. In our experience, this simplifies the induction proofs, and can also remove the need for some intermediate lemmas.
3. Every guard should be total: no input should make it crash, and no input should make it go into an infinite loop. We first discuss how the collection of domain constraints on built-in operations, e.g. array indexing, is justified and propagated to the SMT system. Partiality arising from non-termination of the guard must also be avoided. Current techniques for automatically proving termination, although powerful, can fail, thereby stopping a naive verification process before properties can be proved. We have therefore designed a more supple approach, in which termination proof obligations on user-defined functions are able to be treated in a manner similar to other domain constraints. This allows sound partial correctness proofs for guards, and also allows the SMT backend to be applied to termination proof obligations.