{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T13:59:05Z","timestamp":1726408745543},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319064093"},{"type":"electronic","value":"9783319064109"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06410-9_20","type":"book-chapter","created":{"date-parts":[[2014,4,18]],"date-time":"2014-04-18T17:03:01Z","timestamp":1397840581000},"page":"279-295","source":"Crossref","is-referenced-by-count":7,"title":["Proof Patterns for Formal Methods"],"prefix":"10.1007","author":[{"given":"Leo","family":"Freitas","sequence":"first","affiliation":[]},{"given":"Iain","family":"Whiteside","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","volume-title":"The Event-B book","author":"J.-R. Abrial","year":"2010","unstructured":"Abrial, J.-R.: The Event-B book. Cambridge University Press, UK (2010)"},{"key":"20_CR2","unstructured":"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)"},{"issue":"2","key":"20_CR3","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1147\/sj.352.0151","volume":"35","author":"F.J. Budinsky","year":"1996","unstructured":"Budinsky, F.J., Finnie, M.A., Vlissides, J., Yu, P.: Automatic code generation from design patterns. IBM Systems Journal\u00a035(2), 151\u2013171 (1996)","journal-title":"IBM Systems Journal"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/BFb0012826","volume-title":"9th International Conference on Automated Deduction","author":"A. Bundy","year":"1988","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs. In: Lusk, E., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 111\u2013120. Springer, Heidelberg (1988)"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge Tracts in Theoretical Computer Science, vol.\u00a056. Cambridge University Press (2005)","DOI":"10.1017\/CBO9780511543326"},{"key":"20_CR6","unstructured":"Bundy, A., et al.: Learning from experts to aid the automation of proof search. In: O\u2019Reilly, L., et al. (eds.) PreProceedings of the 9th AVoCS 2009, CSR-2-2009, Swansea University, UK, pp. 229\u2013232 (2009)"},{"key":"20_CR7","volume-title":"Pattern-oriented software architecture: a system of patterns","author":"F. Buschmann","year":"1996","unstructured":"Buschmann, F., et al.: Pattern-oriented software architecture: a system of patterns. John Wiley & Sons, Inc., New York (1996)"},{"issue":"4","key":"20_CR8","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1109\/MS.2007.115","volume":"24","author":"F. Buschmann","year":"2007","unstructured":"Buschmann, F., Henney, K., Schmidt, D.: Past, present, and future trends in software patterns. IEEE Software\u00a024(4), 31\u201337 (2007)","journal-title":"IEEE Software"},{"issue":"4","key":"20_CR9","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/j.scico.2008.09.014","volume":"74","author":"A. Butterfield","year":"2009","unstructured":"Butterfield, A., Freitas, L., Woodcock, J.: Mechanising a formal model of flash memory. Science of Computer Programming\u00a074(4), 219\u2013237 (2009)","journal-title":"Science of Computer Programming"},{"key":"20_CR10","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-45085-6_22","volume-title":"Automated Deduction \u2013 CADE-19","author":"L. Dixon","year":"2003","unstructured":"Dixon, L., Fleuriot, J.: IsaPlanner: A prototype proof planner in isabelle. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 279\u2013283. Springer, Heidelberg (2003)"},{"key":"20_CR11","unstructured":"Freitas, L., Jones, C.B., Velykis, A., Whiteside, I.: How to say why. Technical Report CS-TR-1398, Newcastle University (November 2013), \n                  \n                    http:\/\/www.ai4fm.org\/tr"},{"issue":"5","key":"20_CR12","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/s10009-011-0195-9","volume":"13","author":"L. Freitas","year":"2011","unstructured":"Freitas, L., McDermott, J.: Formal methods for security in the Xenon hypervisor. International Journal on Software Tools for Technology Transfer\u00a013(5), 463\u2013489 (2011)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Freitas, L., Whiteside, I.: Proof patterns for formal methods. Technical Report CS-TR-1399, Newcastle University (November 2013)","DOI":"10.1007\/978-3-319-06410-9_20"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-540-75221-9_11","volume-title":"Formal Methods and Hybrid Real-Time Systems","author":"L. Freitas","year":"2007","unstructured":"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.\u00a04700, pp. 255\u2013279. Springer, Heidelberg (2007)"},{"issue":"1","key":"20_CR15","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/s00165-007-0059-y","volume":"20","author":"L. Freitas","year":"2008","unstructured":"Freitas, L., Woodcock, J.: Mechanising Mondex with Z\/Eves. Formal Aspects of Computing\u00a020(1), 117\u2013139 (2008)","journal-title":"Formal Aspects of Computing"},{"issue":"2-3","key":"20_CR16","first-page":"357","volume":"3","author":"L. Freitas","year":"2009","unstructured":"Freitas, L., Woodcock, J.: A chain datatype in Z. International Journal of Software and Informatics\u00a03(2-3), 357\u2013374 (2009)","journal-title":"International Journal of Software and Informatics"},{"issue":"4","key":"20_CR17","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/j.scico.2008.09.012","volume":"74","author":"L. Freitas","year":"2009","unstructured":"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\u00a074(4), 197\u2013218 (2009)","journal-title":"Science of Computer Programming"},{"issue":"4","key":"20_CR18","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1016\/j.scico.2008.08.001","volume":"74","author":"L. Freitas","year":"2009","unstructured":"Freitas, L., Woodcock, J., Zheng, F.: POSIX file store in Z\/Eves: an experiment in the verified software repository. Science of Computer Programming\u00a074(4), 238\u2013257 (2009)","journal-title":"Science of Computer Programming"},{"key":"20_CR19","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley (1998)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/978-3-642-45221-5_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G. Grov","year":"2013","unstructured":"Grov, G., Kissinger, A., Lin, Y.: A graphical language for proof strategies. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19. LNCS, vol.\u00a08312, pp. 324\u2013339. Springer, Heidelberg (2013)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-39320-4_28","volume-title":"Intelligent Computer Mathematics","author":"J. Heras","year":"2013","unstructured":"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.\u00a07961, pp. 354\u2013358. Springer, Heidelberg (2013)"},{"key":"20_CR22","unstructured":"Heras, J., Komendantskaya, E.: Statistical proof-patterns in Coq\/SSReflect. CoRR, abs\/1301.6039 (2013)"},{"issue":"6","key":"20_CR23","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1093\/jigpal\/11.6.647","volume":"11","author":"M. Jamnik","year":"2003","unstructured":"Jamnik, M.: et\u00a0al. Automatic learning of proof methods in proof planning. Logic Journal of the IGPL\u00a011(6), 647\u2013673 (2003)","journal-title":"Logic Journal of the IGPL"},{"issue":"4","key":"20_CR24","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1109\/MC.2006.145","volume":"39","author":"C. Jones","year":"2006","unstructured":"Jones, C., O\u2019Hearn, P., Woodcock, J.: Verified software: a grand challenge. IEEE Computer\u00a039(4), 93\u201395 (2006)","journal-title":"IEEE Computer"},{"key":"20_CR25","unstructured":"Jones, C.B.: Systematic Software Development using VDM. Prentice Hall (1990)"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-642-39698-4_14","volume-title":"Theories of Programming and Formal Methods","author":"C.B. Jones","year":"2013","unstructured":"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.\u00a08051, pp. 227\u2013243. Springer, Heidelberg (2013)"},{"key":"20_CR27","unstructured":"Jones, C.B., Shaw, R.C.F. (eds.): Case Studies in Systematic Software Development. Prentice Hall International (1990)"},{"key":"20_CR28","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: ACL2 Computer-Aided Reasoning:\u00a0An Approach. University of Austin Texas (2009)"},{"key":"20_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"20_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"20_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/BFb0027284","volume-title":"ZUM\u201997: The Z Formal Specification Notation","author":"M. Saaltink","year":"1997","unstructured":"Saaltink, M.: The Z\/EVES system. In: Till, D., Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol.\u00a01212, pp. 72\u201385. Springer, Heidelberg (1997)"},{"key":"20_CR32","doi-asserted-by":"crossref","unstructured":"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\u201355. ACM (2008)","DOI":"10.1145\/1389449.1389456"},{"key":"20_CR33","unstructured":"Velykis, A.: Inferring the proof process. In: Choppy, C., Delayahe, D., Kla\u00ef, K. (eds.) FM 2012 Doctoral Symposium, Paris, France (August 2012)"},{"key":"20_CR34","unstructured":"Velykis, A.: Capturing & Inferring the Proof Process (under submission). PhD thesis, School of Computing Science, Newcastle University (2014)"},{"key":"20_CR35","unstructured":"Wenzel, M.M.: Isabelle\/Isar - a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"},{"key":"20_CR36","unstructured":"Woodcock, J., Davies, J.: Using Z. Prentice Hall International (1996)"},{"key":"20_CR37","doi-asserted-by":"crossref","unstructured":"Woodcock, J., Freitas, L.: Linking VDM and Z. In: International Conference on Engineering of Complex Computer Systems, Belfast, pp. 143\u2013152 (2008)","DOI":"10.1109\/ICECCS.2008.36"}],"container-title":["Lecture Notes in Computer Science","FM 2014: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06410-9_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T12:52:08Z","timestamp":1558875128000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06410-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319064093","9783319064109"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06410-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}