Advertisement

Program abstraction in a higher-order logic framework

  • Marco Benini
  • Sara Kalvala
  • Dirk Nowotka
Refereed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1479)

Abstract

We present a hybrid approach to program verification: a higher-order logic, used as a specification language, and a human-driven proof environment, with a process-algebraic engine to allow the use of process simulation as an abstraction technique. The domain of application is the validation of object code, and our intent is to adapt and mix existing formalisms to make the verification of representative programs possible. In this paper, we describe the logic in question and an underlying semantics given in terms of a process algebra.

Keywords

Visible Action Program Representation Process Algebra Assembly Language Verification Task 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    J. C. M. Baeten and W. P. Weijland. Process Algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.Google Scholar
  2. 2.
    Michael J. C. Gordon and Tom F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.Google Scholar
  3. 3.
    Robin Milner. An algebraic definition of simulation between programs. In Second Joint Conference on Artificial Intelligence, pages 481–489, 1971.Google Scholar
  4. 4.
    Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.Google Scholar
  5. 5.
    Robin Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, London, 1989.Google Scholar
  6. 6.
    Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Number 828 in LNCS. Springer-Verlag, 1994.Google Scholar
  7. 7.
    Lawrence C. Paulson. A fixedpoint approach to (co)inductive and (co)datatype definitions. Technical Report 304, Computer Laboratory, University of Cambridge, May 1997.Google Scholar
  8. 8.
    Lawrence C. Paulson. Isabelle's object-logics. Technical Report 286, Computer Laboratory, University of Cambridge, May 1997.Google Scholar
  9. 9.
    D. Pavey and L. Winsborrow. Demonstrating equivalence of source code and PROM contents. The Computer Journal, 36(7):654–667, 1993.CrossRefGoogle Scholar
  10. 10.
    David Walker. Bisimulation and divergence. Information and Computation, 85:202–241, 1990.zbMATHMathSciNetCrossRefGoogle Scholar
  11. 11.
    Yuan Yu. Automated proofs of object code for a widely used microprocessor. Research Report 114, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, October 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Marco Benini
    • 1
  • Sara Kalvala
    • 1
  • Dirk Nowotka
    • 1
  1. 1.Department of Computer ScienceUniversity of WarwickCoventryUK

Personalised recommendations