On Fixpoint/Iteration/Variant Induction Principles for Proving Total Correctness of Programs with Denotational Semantics

1. Apt, K.R., Plotkin, G.D.: Countable nondeterminism and random assignment. J. ACM 33(4), 724–767 (1986)

   Article  MathSciNet  Google Scholar 

2. de Bakker, J.W., Scott, D.S.: A theory of programs. IBM Seminar Vienna, Austria, August 1969. Unpublished notes

   Google Scholar 

3. Burstall, R.M.: Program proving as hand simulation with a little induction. In: IFIP Congress, pp. 308–312. North-Holland (1974)

   Google Scholar 

4. Clarke Jr., E.M.: Programming language constructs for which it is impossible to obtain good Hoare axiom systems. J. ACM 26(1), 129–147 (1979)

   Article  MathSciNet  Google Scholar 

5. Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7(1), 70–90 (1978)

   Article  MathSciNet  Google Scholar 

6. Cook, S.A.: Corrigendum: soundness and completeness of an axiom system for program verification. SIAM J. Comput. 10(3), 612 (1981)

   Article  MathSciNet  Google Scholar 

7. Cousot, P.: Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique de programmes. Thèse d’État ès sciences mathématiques, Université de Grenoble Alpes, Grenoble, France, 21 March 1978. (in French)

   Google Scholar 

8. Cousot, P., Cousot, R.: Constructive versions of Tarski’s fixed point theorems. Pac. J. Math. 82(1), 43–57 (1979)

   Article  MathSciNet  Google Scholar 

9. Cousot, P., Cousot, R.: Induction principles for proving invariance properties of programs. In: Néel, D. (ed.) Tools & Notions for Program Construction: An Advanced Course, pp. 75–119. Cambridge University Press, Cambridge (1982)

   Google Scholar 

10. Cousot, P., Cousot, R.: “A la burstall” intermittent assertions induction principles for proving inevitable ability properties of programs. Theor. Comput. Sci. 120(1), 123–155 (1993)

    Article  Google Scholar 

11. Damm, W., Josko, B.: A sound and relatively * complete Hoare-logic for a language with higher type procedures. Acta Inf. 20, 59–101 (1983). https://doi.org/10.1007/BF00264295

    Article  MathSciNet  MATH  Google Scholar 

12. Floyd, R.W.: Assigning meaning to programs. In: Schwartz, J. (ed.) Proceedings of a Symposium in Applied Mathematics, vol. 19, pp. 19–32. American Mathematical Society (1967)

    Google Scholar 

13. Heizmann, M., Jones, N.D., Podelski, A.: Size-change termination and transition invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 22–50. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15769-1_4

    Chapter  Google Scholar 

14. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969). http://doi.acm.org/10.1145/363235.363259

    Article  Google Scholar 

15. Katz, S., Manna, Z.: A closer look at termination. Acta Inf. 5, 333–352 (1975). https://doi.org/10.1007/BF00264565

    Article  MathSciNet  MATH  Google Scholar 

16. Kleene, S.C.: Introduction to Meta-Mathematics. Elsevier North-Holland Pub. Co., Amsterdam (1952)

    Google Scholar 

17. Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL, pp. 81–92. ACM (2001)

    Google Scholar 

18. Leroy, X., Doligez, D., Frisch, A., Garrigue, J., Rémy, D., Vouillon, J.: The OCaml system, release 4.08, Documentation and user’s manual, February 2019. http://caml.inria.fr/pub/docs/manual-ocaml/, copyright \(\copyright \) 2013 Institut National de Recherche en Informatique et en Automatique

19. Manna, Z., Ness, S., Vuillemin, J.: Inductive methods for proving properties of programs. Commun. ACM 16(8), 491–502 (1973)

    Article  MathSciNet  Google Scholar 

20. Manna, Z., Pnueli, A.: Axiomatic approach to total correctness of programs. Acta Inf. 3, 243–263 (1974). https://doi.org/10.1007/BF00288637

    Article  MathSciNet  MATH  Google Scholar 

21. Manna, Z., Vuillemin, J.: Fix point approach to the theory of computation. Commun. ACM 15(7), 528–536 (1972)

    Article  Google Scholar 

22. Markowsky, G.: Chain-complete posets and directed sets with applications. Algebra Univ. 6(1), 53–68 (1976)

    Article  MathSciNet  Google Scholar 

23. Park, D.: On the semantics of fair parallelism. In: Bjøorner, D. (ed.) Abstract Software Specifications. LNCS, vol. 86, pp. 504–526. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10007-5_47

    Chapter  Google Scholar 

24. Régis-Gianas, Y., Pottier, F.: A Hoare logic for call-by-value functional programs. In: Audebaud, P., Paulin-Mohring, C. (eds.) MPC 2008. LNCS, vol. 5133, pp. 305–335. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70594-9_17

    Chapter  Google Scholar 

25. Schmidt, D.W.: Denotational Semantics: A Methodology for Language Development. William C. Brown Publishers, Dubuque (1988). http://people.cs.ksu.edu/~schmidt/text/DenSem-full-book.pdf

    Google Scholar 

26. Scott, D.S.: Outline of a mathematical theory of computation. In: Proceedings of the Fourth Annual Princeton Conference on Information Sciences and Systems, pp. 169–176. Princeton University, March 1970

    Google Scholar 

27. Scott, D.: The lattice of flow diagrams. In: Engeler, E. (ed.) Symposium on Semantics of Algorithmic Languages. LNM, vol. 188, pp. 311–366. Springer, Heidelberg (1971). https://doi.org/10.1007/BFb0059703

    Chapter  Google Scholar 

28. Tarski, A.: A lattice theoretical fixpoint theorem and its applications. Pac. J. Math. 5, 285–310 (1955)

    Article  MathSciNet  Google Scholar 

29. Turing, A.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, University of Cambridge Mathematical Laboratory, Cambridge, England, pp. 67–69 (1949). http://www.turingarchive.org/browse.php/b/8

Download references