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


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
}