References

  1. T. Agerwala & J. Misra (1978): Assertion Graphs for Verifying and Synthesizing Programs. Technical Report 83. University of Texas, Austin, doi:10.1.1.13.1126.
  2. R. Bol (1993): Loop Checking in Partial Deduction. Journal of Logic Programming 16(1–2), pp. 25–46, doi:10.1016/0743-1066(93)90022-9.
  3. P. Cousot & N. Halbwachs (1978): Automatic Discovery of Linear Restraints Among Variables of a Program. In: Proceedings of the ACM Symposium on Principles of Programming Languages, pp. 84–96, doi:10.1145/512760.512770.
  4. S. Das, D.L. Dill & S. Park (1999): Experience With Predicate Abstraction. In: International Conference on Computer Aided Verification, LNCS 1633. Springer, pp. 160–171, doi:10.1007/3-540-48683-6_16.
  5. N. Dershowitz & J.-P. Jouannaud (1990): Rewrite Systems. In: J. van Leeuwen: Handbook of Theoretical Computer Science. Elsevier, pp. 244–320, doi:10.1016/B978-0-444-88074-1.50011-1.
  6. E.W. Dijkstra (1975): Guarded Commands, Nondeterminacy and Formal Derivation of Programs. Communications of the ACM 18, pp. 453–457, doi:10.1145/360933.360975.
  7. M. Ernst, J. Cockrell, W. Griswold & D. Notkin (2001): Dynamically Discovering Likely Program Invariants to Support Program Evolution. IEEE Transactions in Software Engineering 27(2), pp. 1–25, doi:10.1109/32.908957.
  8. C. Flanagan & S. Qadeer (2002): Predicate Abstraction for Software Verification. In: Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM Press, pp. 191–202, doi:10.1145/503272.503291.
  9. R.W. Floyd (1967): Assigning Meanings to Programs. In: Proceedings of the American Mathematical Society Symposia on Applied Mathematics 19, pp. 19–32, doi:10.1090/psapm/019/0235771.
  10. C.A. Furia & B. Meyer (2010): Inferring Loop Invariants Using Postconditions. In: Fields of Logic and Computation. Springer, pp. 277–300, doi:10.1007/978-3-642-15025-8_15.
  11. S. Graf & H. Saidi (1997): Construction of Abstract State Graphs With PVS. In: International Conference on Computer Aided Verification, LNCS 1254. Springer, pp. 72–83, doi:10.1007/3-540-63166-6_10.
  12. G. W. Hamilton (2006): Poitín: Distilling Theorems From Conjectures. Electronic Notes in Theoretical Computer Science 151(1), pp. 143–160, doi:10.1016/j.entcs.2005.11.028.
  13. G.W. Hamilton (2007): Distillation: Extracting the Essence of Programs. In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 61–70, doi:10.1145/1244381.1244391.
  14. G.W. Hamilton (2007): Distilling Programs for Verification. Electronic Notes in Theoretical Computer Science 190(4), pp. 17–32, doi:10.1016/j.entcs.2007.09.005.
  15. G.W. Hamilton & N.D. Jones (2012): Distillation With Labelled Transition Systems. In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. ACM, pp. 15–24, doi:10.1145/2103746.2103753.
  16. G. Higman (1952): Ordering by Divisibility in Abstract Algebras. Proceedings of the London Mathematical Society 2, pp. 326–336, doi:10.1112/plms/s3-2.1.326.
  17. C.A.R. Hoare (1969): An Axiomatic Basis for Computer Programming. Communications of the ACM 12, pp. 576–583, doi:10.1145/363235.363259.
  18. A. Ireland (2006): Towards Automatic Assertion Refinement for Separation Logic. In: Proceedings of the International Conference on Automated Software Engineering, pp. 209–312, doi:10.1109/ASE.2006.69.
  19. A. Ireland & J. Stark (1997): On the Automatic Discovery of Loop Invariants. In: Fourth Nasa Langley Formal Methods Workshop, pp. 137–152, doi:10.1.1.16.9466.
  20. I. Klyuchnikov (2010): Supercompiler HOSC 1.1: Proof of Termination. Preprint 21. Keldysh Institute of Applied Mathematics, Moscow, doi:10.1.1.182.2914.
  21. J.B. Kruskal (1960): Well-Quasi Ordering, the Tree Theorem, and Vazsonyi's Conjecture. Transactions of the American Mathematical Society 95, pp. 210–225, doi:10.2307/1993287.
  22. M. Leuschel (1998): On the Power of Homeomorphic Embedding for Online Termination. In: Proceedings of the International Static Analysis Symposium, Pisa, Italy, pp. 230–245, doi:10.1007/3-540-49727-7_14.
  23. R. Marlet (1994): Vers une Formalisation de l'Évaluation Partielle. Université de Nice - Sophia Antipolis.
  24. P. O'Hearn, J. Reynolds & Y. Hongseok (2001): Local Reasoning About Programs That Alter Data Structures. In: Proceedings of Computer Science Logic, Lecture Notes in Computer Science 2142, pp. 1–19, doi:10.1007/3-540-44802-0_1.
  25. J.C. Reynolds (2002): Separation Logic: A Logic for Shared Mutable Data Structures. In: Proceedings of the Symposium on Logic in Computer Science, pp. 55–74, doi:10.1109/LICS.2002.1029817.
  26. H. Saidi & N. Shankar (1999): Abstract and Model Check While You Prove. In: International Conference on Computer Aided Verification, Lecture Notes in Computer Science 1633. Springer, pp. 443–454, doi:10.1007/3-540-48683-6_38.
  27. S. Sankaranarayanan, H. Sipma & Z. Manna (2004): Non-Linear Loop Invariant Generation Using Gr+.2222emobner Bases. In: Proceedings of the ACM Symposium on Principles of Programming Languages, pp. 318–329, doi:10.1145/964001.964028.
  28. M.H. Sørensen & R. Glück (1994): An Algorithm of Generalization in Positive Supercompilation. Lecture Notes in Computer Science 787, pp. 335–351, doi:10.1.1.49.1869.
  29. M.H. Sørensen, R. Glück & N.D. Jones (1996): A Positive Supercompiler. Journal of Functional Programming 6(6), pp. 811–838, doi:10.1017/S0956796800002008.
  30. N. Suzuki & K. Ishihata (1977): Implementation of an Array Bound Checker. In: 4th ACM Symposium on Principles of Programming Languages. ACM Press, pp. 132–143, doi:10.1145/512950.512963.
  31. Z. Xu & B. Reps, T. amd Miller (2000): Safety Checking of Machine Code. In: ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM Press, pp. 70–82, doi:10.1145/349299.349313.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org