Proof Patterns for Formal Methods

1. Abrial, J.-R.: The Event-B book. Cambridge University Press, UK (2010)

   Google Scholar 

2. Alexander, C., Ishikawa, S., Silverstein, M.: A Pattern Language: Towns, Buildings, Construction (Center for Environmental Structure Series). Oxford University Press (August 1977) (later printing edition)

   Google Scholar 

3. Budinsky, F.J., Finnie, M.A., Vlissides, J., Yu, P.: Automatic code generation from design patterns. IBM Systems Journal 35(2), 151–171 (1996)

   Article  Google Scholar 

4. Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 111–120. Springer, Heidelberg (1988)

   Chapter  Google Scholar 

5. Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge Tracts in Theoretical Computer Science, vol. 56. Cambridge University Press (2005)

   Google Scholar 

6. Bundy, A., et al.: Learning from experts to aid the automation of proof search. In: O’Reilly, L., et al. (eds.) PreProceedings of the 9th AVoCS 2009, CSR-2-2009, Swansea University, UK, pp. 229–232 (2009)

   Google Scholar 

7. Buschmann, F., et al.: Pattern-oriented software architecture: a system of patterns. John Wiley & Sons, Inc., New York (1996)

   Google Scholar 

8. Buschmann, F., Henney, K., Schmidt, D.: Past, present, and future trends in software patterns. IEEE Software 24(4), 31–37 (2007)

   Article  Google Scholar 

9. Butterfield, A., Freitas, L., Woodcock, J.: Mechanising a formal model of flash memory. Science of Computer Programming 74(4), 219–237 (2009)

   Article  MATH  MathSciNet  Google Scholar 

10. Dixon, L., Fleuriot, J.: IsaPlanner: A prototype proof planner in isabelle. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 279–283. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

11. Freitas, L., Jones, C.B., Velykis, A., Whiteside, I.: How to say why. Technical Report CS-TR-1398, Newcastle University (November 2013), http://www.ai4fm.org/tr

12. Freitas, L., McDermott, J.: Formal methods for security in the Xenon hypervisor. International Journal on Software Tools for Technology Transfer 13(5), 463–489 (2011)

    Article  Google Scholar 

13. Freitas, L., Whiteside, I.: Proof patterns for formal methods. Technical Report CS-TR-1399, Newcastle University (November 2013)

    Google Scholar 

14. Freitas, L., Woodcock, J.: Proving theorems about JML classes. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems. LNCS, vol. 4700, pp. 255–279. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

15. Freitas, L., Woodcock, J.: Mechanising Mondex with Z/Eves. Formal Aspects of Computing 20(1), 117–139 (2008)

    Article  Google Scholar 

16. Freitas, L., Woodcock, J.: A chain datatype in Z. International Journal of Software and Informatics 3(2-3), 357–374 (2009)

    Google Scholar 

17. Freitas, L., Woodcock, J., Zhang, Y.: Verifying the CICS file control API with Z/Eves: an experiment in the verified software repository. Science of Computer Programming 74(4), 197–218 (2009)

    Article  MATH  MathSciNet  Google Scholar 

18. Freitas, L., Woodcock, J., Zheng, F.: POSIX file store in Z/Eves: an experiment in the verified software repository. Science of Computer Programming 74(4), 238–257 (2009)

    Article  MATH  MathSciNet  Google Scholar 

19. Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley (1998)

    Google Scholar 

20. Grov, G., Kissinger, A., Lin, Y.: A graphical language for proof strategies. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19. LNCS, vol. 8312, pp. 324–339. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

21. Heras, J., Komendantskaya, E.: ML4PG in computer algebra verification. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS, vol. 7961, pp. 354–358. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

22. Heras, J., Komendantskaya, E.: Statistical proof-patterns in Coq/SSReflect. CoRR, abs/1301.6039 (2013)

    Google Scholar 

23. Jamnik, M.: et al. Automatic learning of proof methods in proof planning. Logic Journal of the IGPL 11(6), 647–673 (2003)

    Article  MATH  MathSciNet  Google Scholar 

24. Jones, C., O’Hearn, P., Woodcock, J.: Verified software: a grand challenge. IEEE Computer 39(4), 93–95 (2006)

    Article  Google Scholar 

25. Jones, C.B.: Systematic Software Development using VDM. Prentice Hall (1990)

    Google Scholar 

26. Jones, C.B., Freitas, L., Velykis, A.: Ours is to reason why. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 227–243. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

27. Jones, C.B., Shaw, R.C.F. (eds.): Case Studies in Systematic Software Development. Prentice Hall International (1990)

    Google Scholar 

28. Kaufmann, M., Manolios, P., Moore, J.S.: ACL2 Computer-Aided Reasoning: An Approach. University of Austin Texas (2009)

    Google Scholar 

29. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)

    Book  MATH  Google Scholar 

30. Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)

    Book  MATH  Google Scholar 

31. Saaltink, M.: The Z/EVES system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 72–85. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

32. Silva, P.F., Oliveira, J.N.: Galculator: functional prototype of a Galois-connection based proof assistant. In: Antoy, S., Albert, E. (eds.) PPDP, pp. 44–55. ACM (2008)

    Google Scholar 

33. Velykis, A.: Inferring the proof process. In: Choppy, C., Delayahe, D., Klaï, K. (eds.) FM 2012 Doctoral Symposium, Paris, France (August 2012)

    Google Scholar 

34. Velykis, A.: Capturing & Inferring the Proof Process (under submission). PhD thesis, School of Computing Science, Newcastle University (2014)

    Google Scholar 

35. Wenzel, M.M.: Isabelle/Isar - a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universität München (2002)

    Google Scholar 

36. Woodcock, J., Davies, J.: Using Z. Prentice Hall International (1996)

    Google Scholar 

37. Woodcock, J., Freitas, L.: Linking VDM and Z. In: International Conference on Engineering of Complex Computer Systems, Belfast, pp. 143–152 (2008)

    Google Scholar 

Download references