Machine assisted proofs of properties of Avalon programs

Abstract: "Proving the correctness of programs by hand is hard and error-prone. How can mechanical theorem proving aids such as the Larch Prover (LP) help in the proofs of complex programs? We address this question by applying LP, a proof checker based on rewrite-rule theory, to the proof of an Avalon/C++ program. Avalon/C++ is a programming language that supports concurrency and fault-tolerance through transaction-based computations. Since reasoning about an Avalon/C++ program requires reasoning about histories, i.e., sequences of operations, and not just initial and final states, proofs of correctness are non-trivial. For the Avalon/C++ queue example, we present a formal Larch Shared Language specification, which we also used as input to LP. We discuss the LP-assisted proofs we performed of the representation invariant and the queue's key correctness condition, give detailed statistics of our proofs, and draw some conclusions based on our experience with LP."