Program Refinement by Theorem Prover

1. M. Aagard and M. Leeser. Verifying a logic synthesis tool in Nuprl. In Proc. 4th Workshop on Computer-Aided Verification,Montreal, Canada, June 1992. Springer-Verlag.

   Google Scholar 

2. S. Agerholm. Mechanizing program verification in HOL. DAIMI IR-111, Aarhus University, Apr. 1992.

   Google Scholar 

3. F. Andersen. A Theorem Prover for UNITY in Higher Order Logic. PhD thesis, Technical University of Denmark, Lyngby, Denmark, Mar. 1992.

   Google Scholar 

4. R.J.R. Back. Correctness Preserving Program Refinements: Proof Theory and Applications, volume 131 of Mathematical Center Tracts. Mathematical Centre, Amsterdam, 1980.

   Google Scholar 

5. R.J.R. Back. A calculus of refinements for program derivations. Acta Informatica, 25: 593–624, 1988.

   Article  MathSciNet  MATH  Google Scholar 

6. R.J.R. Back. Changing data representation in the refinement calculus. In 21st Hawaii International Conference on System Sciences, January 1989.

   Google Scholar 

7. R.J.R. Back. Refinement calculus, part II: Parallel and reactive programs. In REX Workshop for Refinement of Distributed Systems,volume 430 of Lecture Notes in Computer Science,Nijmegen, The Netherlands, 1989. Springer—Verlag.

   Google Scholar 

8. R.J.R. Back and K. Sere. Superposition refinement of parallel algorithms. In K.R. Parker and G.A. Rose, editors, Formal Description Techniques IV, pages 475–493. Elsevier Science Publishers (North-Holland), 1992.

   Google Scholar 

9. R.J.R. Back and J. von Wright. Refinement calculus, part I: Sequential programs. In REX Workshop for Refinement of Distributed Systems,volume 430 of Lecture Notes in Computer Science,Nijmegen, The Netherlands, 1989. Springer—Verlag.

   Google Scholar 

10. R.J.R. Back and J. von Wright. Refinement concepts formalised in higher-order logic. Formal Aspects of Computing, 2: 247–272, 1990.

    Article  Google Scholar 

11. R.J.R. Back and J. von Wright. Statement inversion and strongest post-condition Science of Computer Programming, 20: 223–251, 1993.

    Article  MathSciNet  MATH  Google Scholar 

12. R.J.R. Back and J. von Wright. Combining angels, demons and miracles in program specifications. Theoretical Computer Science, 100: 365–383, 1992.

    Article  MathSciNet  MATH  Google Scholar 

13. A.J. Camilleri. Mechanizing CSP trace theory in higher order logic. IEEE Transactions of Software Engineering, 16 (9): 993–1004, 1990.

    Article  Google Scholar 

14. A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5: 56–68, 1940.

    Article  MathSciNet  MATH  Google Scholar 

15. E.W. Dijkstra. A Discipline of Programming. Prentice—Hall International, 1976.

    Google Scholar 

16. E.W. Dijkstra and A.J.M. van Gasteren. A simple fixpoint argument without the restriction to continuity. Acta Informatica, 23: 1–7, 1986.

    Article  MathSciNet  MATH  Google Scholar 

17. U. Engberg, P. Groenning and L. Lamport. Mechanical verification of concurrent systems with TLA. In Proc. ,nth Workshop on Computer-Aided Verification,Montreal, Canada, June 1992. Springer-Verlag.

    Google Scholar 

18. P.H. Gardiner and C.C. Morgan. Data refinement of predicate transformers. Theoretical Computer Science, 87 (1): 143–162, 1991.

    Article  MathSciNet  MATH  Google Scholar 

19. D. M. Goldschlag. Mechanizing UNITY. In M. Broy, editor, TC2 Working Conference on Programming Concepts and Methods, pages 374–401, Israel, 1990. IFIP.

    Google Scholar 

20. M.J.C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwistle and P.A. Subrahmanyam (ed.), VLSI Specification, Verification and Synthesis. Kluwer Academic Publishers, 1988.

    Google Scholar 

21. M.J.C. Gordon. Mechanizing programming logics in higher-order logic. In G. Birtwistle and P.A. Subrahmanyam (ed.), Current Trends in Hardware Verification and Theorem Proving. Springer-Verlag, 1989.

    Google Scholar 

22. L. Groves and R. Nickson. A tactic driven refinement tool. In Jones et al, editor, Proc. 5th Refinement Workshop,London, Jan. 1992. Springer—Verlag.

    Google Scholar 

23. J. Grundy. A window inference tool for refinement. In Jones et al, editor, Proc. 5th Refinement Workshop, London, Jan. 1992. Springer-Verlag.

    Google Scholar 

24. C.A.R. Hoare. Proofs of correctness of data representation. Acta Informatica, 1 (4): 271–281, 1972.

    Article  MATH  Google Scholar 

25. C.B. Jones. Systematic Software Development Using VDM. Prentice-Hall International, 1986.

    Google Scholar 

26. C.C. Morgan. Data refinement by miracles. Information Processing Letters, 26: 243–246, January 1988.

    Article  MathSciNet  Google Scholar 

27. C.C. Morgan. Programming from Specifications. Prentice-Hall, 1990.

    Google Scholar 

28. J.M. Morris. Laws of data refinement. Acta Informatica, 26: 287–308, 1989.

    MathSciNet  MATH  Google Scholar 

29. P.J. Robinson and J. Staples. Formalising the hierarchical structure of practical mathematical reasoning. Techn. Rep. 138, Key Centre for Software Technology, University of Queensland, Australia, 1990.

    Google Scholar 

30. T. Vickers. An overview of a refinement editor. In 5th Australian Software Engineering Conference, Sydney, May 1990.

    Google Scholar 

31. J. von Wright. The lattice of data refinement. Reports on computer science and mathematics 130, Abo Akademi, 1992. To appear in Acta Informatica.

    Google Scholar 

32. J. von Wright, J. Hekanaho, P. Luostarinen and T. Lângbacka. Mechanising some advanced refinement concepts. Formal Methods in System Design, 3: 49–81, 1993.

    Article  MATH  Google Scholar 

Download references