Automata as Proofs

摘要

A recent approach to the verification of programs constructs a correctness proof in the form of a finite automaton. The automaton recognizes a set of traces. Here, a trace is any sequence of statements (not necessarily feasible and not necessarily on a path in the control flow graph of the program). A trace can be formalized as a word over the alphabet of statements. A trace can also be viewed as as special case of a program. Applying static analysis or a symbolic method (e.g., SMT solving with interpolant generation) to a single trace τ, a correctness proof for the trace τ can be obtained in the form of a sequence of consecutive Hoare triples (or, phrased differently, an inductive sequence of assertions). We can construct an automaton that contains a transition qΦa /→ qΦ' for each Hoare triple {Φ}a{Φ'} in the correctness proof for the trace τ. The automaton accepts the trace τ. In fact, the automaton accepts all traces whose correctness proof uses the same set of Hoare triples as the trace τ. Given a program and a number of traces τ_1,..., τ_n of the program, we can construct an automaton from the n different correctness proofs for the traces τ_1,..., τ_n. The automaton recognizes a set of correct traces. We still need to check whether this set includes all the traces on a path in the control flow graph of the program. The check is an automata-theoretic operation (which is reducible to nonreachability in a finite graph). That is, the two steps of constructing and checking a proof neatly separate the two concerns of data and control in program verification. The construction of a proof in the form of an automaton accounts for the interpretation of statements in data domains. The automaton, however, has a meaning that is oblivious to the interpretation of statements: a set of words over a particular alphabet. The check of the proof uses this meaning of the automaton and accounts for the control flow of the program. The implementation of the check of the proof as an automata-theoretic inclusion check is reminiscent of model checking (the finite control flow graph defines the model, the automaton defines the property). The resulting verification method is not compositional in the syntax of the program; it is compositional in a new, semantics-directed sense where modules are sets of traces; the sets of traces are constructed from mutually independent correctness proofs and intuitively correspond to different cases of program executions. Depending on the verification problem (the correctness property being safety or termination for sequential, recursive, or concurrent programs), the approach uses non-deterministic automata, nested-word automata, Büchi automata, or alternating automata as proofs; see, e.g., [2,3,1].