Proof Styles in Operational Semantics
S. Ray and J S. Moore
In A. J. Hu and
A. K. Martin, editors, Proceedings of the 5th International Conference on
Formal Methods in Computer-aided Design (FMCAD 2004), Austin, TX,
November 2004, volume 3312 of LNCS, pages
67-81. Springer.
© Springer-Verlag Berlin
Heidelberg 2004.
Abstract
We relate two well-studied methodologies in deductive verification of
operationally modeled sequential programs, namely the use of inductive invariants and clock functions. We prove that the two
methodologies are equivalent in the following sense: If the logic used is
sufficiently expressive then one can mechanically transform a proof of a
program in one methodology to a proof in the other. Both partial and total
correctness are considered. We also show that the mechanical transformation is
compositional in that different parts of a program can be verified using
different methodologies to achieve a complete proof of the entire program. Our
proof of equivalence has been mechanically verified by the ACL2 theorem prover
and we discuss automatic tools in the form of ACL2 macros to carry out the
transformation between the two methodologies in the ACL2 system.
Relevant files
- Paper (ps, pdf)
- Slides for FMCAD 2004 (ps, pdf)
- Supporting ACL2 proof
scripts: See the directory
books/proofstyles/invclock/
in
the current ACL2 distribution.
BibTex
@Inproceedings{ray-proof,
author = "S. Ray and J S. Moore",
title = "{Proof Styles in Operational Semantics}",
editor = "A. J. Hu and A. K. Martin",
booktitle = "{Proceedings of the $5$th International Conference on
Formal Methods in Computer-Aided Design (FMCAD 2004)}",
series = "{LNCS}",
volume = "3312",
address = "{Austin, TX}",
publisher = "{Springer}",
month = nov,
pages = "67-81",
year = 2004
}