Skip to main content
SpringerLink
Log in

Tracing the origins of verification conditions

  • Conference
  • Conference paper
  • First Online:
Algebraic Methodology and Software Technology (AMAST 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1101))

Abstract

The typical program verification sytem is a batch tool that accepts as input a program annotated with Floyd-Hoare assertions, performs syntactic and semantic analysis on it, and generates a list of verification conditions that is subsequently submitted to a theorem prover. When a verification condition cannot be proved, this may be due to an error in the program or an inconsistency in the annotations. Unfortunately, it is very difficult to relate a failing proof attempt to a particular piece of code or assertion. We propose a solution to this problem using the technique of origin tracking.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J-R. Abrial. The B-Book. Assigning Programs to Meanings. Cambridge University Press, 1995. (to appear).

    Google Scholar 

  2. Y. Bertot. Occurrences in Debugger Specifications. In ACM SIGPLAN Conference on Programming Language Design and Implementation, 1991.

    Google Scholar 

  3. Y. Bertot. Une Automatisation du Calcul des Résidus en Sémantique Naturelle. PhD thesis, Université de Nice-Sophia Antipolis, 1991.

    Google Scholar 

  4. Y. Bertot. Origin Functions in λ-calculus and Term Rewriting Systems. In CAAP'92, 1992. Springer Verlag LNCS 581.

    Google Scholar 

  5. Y. Bertot. A Canonical Calculus of Residuals. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 147–163. Cambridge University Press, 1993. (also appears as INRIA Report no. 1542, Oct. 1991).

    Google Scholar 

  6. T. Despeyroux. Executable Specifications of Static Semantics. In International Symposium on Semantics of Data Types, 1984. Springer-Verlag LNCS 173.

    Google Scholar 

  7. E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

    Google Scholar 

  8. A.V. Deursen, P. Klint, and F. Tip. Origin Tracking. In Journal of Symbolic Computation, volume 15, pages 523–545, 1993.

    Google Scholar 

  9. R.W. Floyd. Assigning Meanings to Programs. In J.T. Schwartz, editor, Mathematical Aspects of Computer Science: Proceedings of the 19th Symposium in Applied Mathematics, pages 19–32, Providence, United States, 1966.

    Google Scholar 

  10. D. Guaspari, C. Marceau, and W. Polak. Formal Verification of Acta Programs. In IEEE Transactions on Software Engineering, volume 16, pages 1058–1075, September 1990.

    Google Scholar 

  11. D.I. Good. Mechanical Proofs about Computer Programs. In C.A.R. Hoare and J.C. Sheperdson, editors, Mathematical Logic and Programming Languages. Prentice Hall, 1985.

    Google Scholar 

  12. C.A.R. Hoare. An Axiomatic Basis for Computer Programming. In Communications of the ACM, October 1969.

    Google Scholar 

  13. S. Igarashi, R.L. London, and D.C. Luckham. Automatic Program Verification: A Logical Basis and its Implementation. In Acta Informatica, volume 4, pages 145–182, 1975.

    Google Scholar 

  14. I. Jacobs. The Centaur Reference Manual. Technical report, INRIA, Sophia-Antipolis, 1994.

    Google Scholar 

  15. I. Jacobs, F. Montagnac, J. Bertot, and D. Clement. The Sophtalk Reference Manual. Technical Report 150, INRIA, Sophia-Antipolis, 1993.

    Google Scholar 

  16. C. Jones. Systematic Software Development using VDM. Prentice-Hall, 1986.

    Google Scholar 

  17. P. Klint. A Meta-environment for Generating Programming Environments. In ACM Transaction on Software Engineering and Methodology, volume 2, pages 176–201, 1993.

    Google Scholar 

  18. S. Kromodimoeljo, B. Pase, M. Saaltink, D. Craigen, and I. Meisels. The EVES System. In Proceedings of the International Lecture Series on Functional Programming, Concurrency, Simulation and Automated Reasoning, 1992.

    Google Scholar 

  19. T. Reps and T. Teitelbaum. The Synthesizer Generator: a System for Constructing Language Based Editors. Springer Verlag, 1988. (third edition).

    Google Scholar 

  20. M. Weiser. Program Slicing. In IEEE Transactions on Software Engineering, volume 10, page 352, 1984.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA, 2004 Route des Lucioles, 06902, Sophia-Antipolis, France

    Ranan Fraer

Authors
  1. Ranan Fraer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Martin Wirsing Maurice Nivat

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fraer, R. (1996). Tracing the origins of verification conditions. In: Wirsing, M., Nivat, M. (eds) Algebraic Methodology and Software Technology. AMAST 1996. Lecture Notes in Computer Science, vol 1101. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014320

Download citation

  • DOI: https://doi.org/10.1007/BFb0014320

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61463-0

  • Online ISBN: 978-3-540-68595-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation