PAMELA+PVS Verification of Sequential Programs

  • Bettina Buth
Conference paper
Part of the Advances in Computing Science book series (ACS)


Tool support is an essential requirement for the applicability of Formal Methods to realistic, large-scale systems, and the acceptance of Formal Methods in industries in general. Many examples demonstrate how useful the currently existing tools can be especially during the specification and design phase. Essential prerequisites are modularity and scalability of the underlying method. Due to the availability of mature methods and related tools the interest of the Formal Methods community has shifted from the development of new methods to linking of theories and the combination of tools. In this paper an example for the combined use of existing tools is presented, namely the verification condition generator PAMELA (see Buth (1995)) and the proof checker PVS (see Crow


Operational Semantic Recursive Call Sequential Program Proof Obligation Symbolic Execution 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. Bjørner D., Hoare, C. A. R., Bowen, J., He, J., Langmaack, H., Olderog, E.-R., Martin, U., Stravridou, V., Nielson, F., Nielson, 11.-R., Barringer, H., Edwards, D., LOvengreen, 11.-H., Ravn, A. P., and Rischel, H. (1989): A ProCoS project description–ESPRIT BRA 3014. Bulletin of the EATCS 39, 60–73.Google Scholar
  2. Buth, B., Buth, K.H., Martin, U., and Stavridou, V. (1989): Experiments with program verification systems. ProCoS Technical Report Kiel BB2, Christian-Albrechts-Universität Kiel.Google Scholar
  3. Buth, B. (1995): Operation Refinement Proofs for VDM-like Specifications, Dissertation; published as Technical Report 9501 Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel. (see also:
  4. Buth, B. (1998): An Interface between PAMELA and PVS, Report, in preparation. Buth, B., Cardell-Oliver, R., and Peleska, J. (1998): Combining Tools for the Verification of Fault-Tolerant Systems. In: Tools for System Development and Verification, (Workshop Proceedings), BISS Monographs, Shaker, 1998.Google Scholar
  5. Crow,J., Owre,S., Rushby, J., Shankar,S., and Srivas,M. (1995): A Tutorial Introduction to PVS, Presented at WIFT ‘85: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida; (see also:
  6. de Bakker, J.-W. (1980): Mathematical Theory of Program Correctness. Series in Computer Science. Prentice-Hall International.Google Scholar
  7. Hoare, C.A.R. (1985): Communicating Sequential Processes; Prentice Hall International.Google Scholar
  8. Jones, C.B. (1990): Systematic Software Development using VDM, Series in Computer Science. Prentice-Hall International, Second Edition.Google Scholar
  9. Heisel, M., Reif, W., and Stephan, W. (1990) Tactical theorem proving in program verification. in Stickel, M. E. (ed.) Proceedings of the 10th International Conference on Automated Deduction, Kaiserslautern, FRG, LNAI 449, pp 117–131. Springer-Verlag.Google Scholar
  10. Peleska, J. and Siegel, M. (1996): Test Automation of Safety-Critical Reactive Systems. South African Computer Jounal (1997) 19: 53–77. Also available as Bericht Nr. 9614, Dezember 1996, Institut für Informatik und praktische Mathematik, Christian¬Albrechts-Universität Kiel.Google Scholar
  11. Peleska, J. (1996): Formal Methods and the Development of Dependable Systems; Habil itationsschrift, Technical Report 9612, Institut für Informatik, Christian-Albrechts Universität Kiel; (see also: http://www. Scholar
  12. The RAISE Method Group (1995): The RAISE Development Method. The Practitioner Series, Prentice Hall.Google Scholar
  13. Weber-Wulff, D. (1993): Proof movie - a proof with the Boyer-Moore Prover. in:Forrnal Aspects of Computing 5(2), 121–151.Google Scholar

Copyright information

© Springer-Verlag Wien 1999

Authors and Affiliations

  • Bettina Buth

There are no affiliations available

Personalised recommendations