Tracing the origins of verification conditions

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