Machine assisted proofs of properties of Avalon programs

Author / Creator

Wing, Jeannette Marie

Available as

Physical

Summary

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 addr...

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."

Show More