Carnegie Mellon University
file.pdf (1.61 MB)

Machine assisted proofs of properties of Avalon programs

Download (1.61 MB)
journal contribution
posted on 2004-08-01, 00:00 authored by Jeannette Marie. Wing, Chun Gong
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."




Usage metrics