{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T14:23:13Z","timestamp":1726410193552},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642396977"},{"type":"electronic","value":"9783642396984"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39698-4_14","type":"book-chapter","created":{"date-parts":[[2013,7,24]],"date-time":"2013-07-24T13:03:05Z","timestamp":1374670985000},"page":"227-243","source":"Crossref","is-referenced-by-count":3,"title":["Ours Is to Reason Why"],"prefix":"10.1007","author":[{"given":"Cliff B.","family":"Jones","sequence":"first","affiliation":[]},{"given":"Leo","family":"Freitas","sequence":"additional","affiliation":[]},{"given":"Andrius","family":"Velykis","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","volume-title":"The Event-B Book","author":"J.-R. Abrial","year":"2010","unstructured":"Abrial, J.-R.: The Event-B Book. Cambridge University Press, Cambridge (2010)"},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/BF00264250","volume":"21","author":"H. Barringer","year":"1984","unstructured":"Barringer, H., Cheng, J.H., Jones, C.B.: A logic covering undefinedness in program proofs. Acta Informatica\u00a021, 251\u2013269 (1984)","journal-title":"Acta Informatica"},{"key":"14_CR3","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":"14_CR4","unstructured":"Bundy, A., Grov, G., Jones, C.B.: Learning from experts to aid the automation of proof search. In: O\u2019Reilly, L., Roggenbach, M. (eds.) AVoCS 2009 \u2013 PreProceedings of the Ninth International Workshop on Automated Verification of Critical Systems, CSR-2-2009, pp. 229\u2013232. Swansea University (2009)"},{"key":"14_CR5","unstructured":"Bundy, A., Grov, G., Jones, C.B.: An outline of a proposed system that learns from experts how to discharge proof obligations automatically. In: Abrial, J.-R., Butler, M., Joshi, R., Troubitsyna, E., Woodcock, J.C.P. (eds.) Dagstuhl 09381: Refinement Based Methods for the Construction of Dependable Systems, pp. 38\u201342 (2009)"},{"key":"14_CR6","unstructured":"Freitas, L., Jones, C.B.: Learning from an expert\u2019s proof: AI4FM. In: Ball, T., Zuck, L., Shankar, N. (eds.) UV 2010 (Usable Verification) (November 2010)"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Guttag, J.V., Horning, J.J., Garl, W.J., Jones, K.D., Modet, A., Wing, J.M.: Larch: languages and tools for formal specification. Springer (1993)","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"14_CR8","unstructured":"Jackson, M.: Problem Frames: Analyzing and structuring software development problems. Addison-Wesley (2000)"},{"key":"14_CR9","unstructured":"Jones, C.B.: Software Development: A Rigorous Approach. Prentice Hall International (1980)"},{"key":"14_CR10","unstructured":"Jones, C.B.: Systematic Software Development using VDM, 2nd edn. Prentice Hall International (1990)"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Jones, C.B., Jones, K.D., Lindsay, P.A., Moore, R.: mural: A Formal Development Support System. Springer (1991)","DOI":"10.1007\/978-1-4471-3180-9"},{"key":"14_CR12","unstructured":"Jones, C.B., Shaw, R.C.F. (eds.): Case Studies in Systematic Software Development. Prentice Hall International (1990)"},{"key":"14_CR13","unstructured":"Jones, C.B., Grov, G., Bundy, A.: Ideas for a high-level proof strategy language. In: Dutertre, B., Saidi, H. (eds.) AFM 2010 (Automated Formal Methods) (July 2010)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-540-75221-9_16","volume-title":"Formal Methods and Hybrid Real-Time Systems","author":"C.B. Jones","year":"2007","unstructured":"Jones, C.B., Hayes, I.J., Jackson, M.A.: Deriving specifications for systems that are connected to the physical world. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) Formal Methods and Hybrid Real-Time Systems. LNCS, vol.\u00a04700, pp. 364\u2013390. Springer, Heidelberg (2007)"},{"key":"14_CR15","unstructured":"Kaufmann, M., Manolios, P., Strother Moore, J.: ACL2 Computer-Aided Reasoning: An Approach. University of Austin Texas (2009)"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"14_CR18","unstructured":"Rodin: The Rodin Tools can be downloaded from SourceForge (2008), \n                  \n                    http:\/\/www.sourceforge.net\/projects\/rodin-b-sharp"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Romanovsky, A., Thomas, M. (eds.): Industrial Deployment of System Engineering Methods. Springer (2013)","DOI":"10.1007\/978-3-642-33170-1"},{"key":"14_CR20","unstructured":"Schmalz, M.: Formalising the Logic of Event-B. PhD thesis, ETH, Zuerich (2012)"},{"key":"14_CR21","unstructured":"Velykis, A.: Isabelle\/Eclipse (2013), \n                  \n                    http:\/\/andriusvelykis.github.io\/isabelle-eclipse"},{"key":"14_CR22","unstructured":"Velykis, A., Freitas, L., Jones, C.B., Whiteside, I.: How to say why (in AI4FM). Technical Report CS-TR-1376, Newcastle University (March 2013)"},{"key":"14_CR23","unstructured":"WWW. AI4FM (February 2013), \n                  \n                    http:\/\/www.ai4fm.org"},{"key":"14_CR24","unstructured":"WWW. Deploy project web site (February 2013), \n                  \n                    http:\/\/www.ncl.ac.uk\/computing\/research\/project\/3625"},{"key":"14_CR25","unstructured":"WWW. Overture (March 2013) \n                  \n                    http:\/\/www.overturetool.org"},{"key":"14_CR26","unstructured":"WWW. The ProB animator and model checker (February 2013), \n                  \n                    http:\/\/www.stups.uni-duesseldorf.de\/ProB"}],"container-title":["Lecture Notes in Computer Science","Theories of Programming and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39698-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T23:05:08Z","timestamp":1557961508000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39698-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396977","9783642396984"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39698-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}