{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:48:42Z","timestamp":1740098922572,"version":"3.37.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319668444"},{"type":"electronic","value":"9783319668451"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66845-1_5","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:37:20Z","timestamp":1503747440000},"page":"69-84","source":"Crossref","is-referenced-by-count":5,"title":["Making Whiley Boogie!"],"prefix":"10.1007","author":[{"given":"Mark","family":"Utting","sequence":"first","affiliation":[]},{"given":"David J.","family":"Pearce","sequence":"additional","affiliation":[]},{"given":"Lindsay","family":"Groves","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-319-33693-0_6","volume-title":"Integrated Formal Methods","author":"M Ameri","year":"2016","unstructured":"Ameri, M., Furia, C.A.: Why just Boogie? In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 79\u201395. Springer, Cham (2016). doi:\n10.1007\/978-3-319-33693-0_6"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Arlt, S., R\u00fcmmer, P., Sch\u00e4f, M.: Joogie: from Java through Jimple to Boogie. In: Proceedings of SOAP (2013)","DOI":"10.1145\/2487568.2487570"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). doi:\n10.1007\/11804192_17"},{"issue":"6","key":"5_CR4","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1145\/1953122.1953145","volume":"54","author":"M Barnett","year":"2011","unstructured":"Barnett, M., F\u00e4hndrich, M., Leino, K.R.M., M\u00fcller, P., Schulte, W., Venter, H.: Specification and verification: the Spec# experience. CACM 54(6), 81\u201391 (2011)","journal-title":"CACM"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Betts, A., Chong, N., Donaldson, A.F., Qadeer, S., Thomson, P.: GPUVerify: a verifier for GPU kernels. In: Proceedings of the OOPSLA, pp. 113\u2013132. ACM Press (2012)","DOI":"10.1145\/2384616.2384625"},{"key":"5_CR6","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Workshop on Intermediate Verification Languages (2011)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009). doi:\n10.1007\/978-3-642-03359-9_2"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"DR Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108\u2013128. Springer, Heidelberg (2005). doi:\n10.1007\/978-3-540-30569-9_6"},{"issue":"3","key":"5_CR9","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. JACM 52(3), 365\u2013473 (2005)","journal-title":"JACM"},{"key":"5_CR10","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. SRC Research Report 159, Compaq Systems Research Center (1998)"},{"key":"5_CR11","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminancy and formal derivation of programs. CACM 18, 453\u2013457 (1975)","journal-title":"CACM"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81\u201394. Springer, Heidelberg (2006). doi:\n10.1007\/11817963_11"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J., Paskevich, A.: Why3 \u2013 where programs meet provers. In: Proceedings of ESOP, pp. 125\u2013128 (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of PLDI, pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"issue":"1","key":"5_CR15","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"C Hoare","year":"2003","unstructured":"Hoare, C.: The verifying compiler: a grand challenge for computing research. JACM 50(1), 63\u201369 (2003)","journal-title":"JACM"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-20398-5_4"},{"key":"5_CR17","unstructured":"Leino, K.R.M.: Ecstatic: an object-oriented programming language with an axiomatic semantics. In: Workshop on Foundations of Object-Oriented Languages (FOOL 4) (1997)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-17511-4_20"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Program proving using intermediate verification languages (IVLs) like Boogie and Why3. In: Proceedings of HILT, pp. 25\u201326 (2012)","DOI":"10.1145\/2402676.2402689"},{"key":"5_CR20","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139629294","volume-title":"Building High Integrity Applications with SPARK","author":"JW McCormick","year":"2015","unstructured":"McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press, Cambridge (2015)"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). doi:\n10.1007\/978-3-540-78800-3_24"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L Moura","year":"2007","unstructured":"Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 183\u2013198. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-73595-3_13"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). doi:\n10.1007\/978-3-662-49122-5_2"},{"key":"5_CR24","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. JACM 27, 356\u2013364 (1980)","journal-title":"JACM"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-642-35873-9_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"DJ Pearce","year":"2013","unstructured":"Pearce, D.J.: Sound and complete flow typing with unions, intersections and negations. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 335\u2013354. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-35873-9_21"},{"key":"5_CR26","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/j.scico.2015.09.006","volume":"113","author":"DJ Pearce","year":"2015","unstructured":"Pearce, D.J., Groves, L.: Designing a verifying compiler: lessons learned from developing Whiley. Sci. Comput. Program. 113, 191\u2013220 (2015)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"5_CR27","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1093\/logcom\/3.1.47","volume":"3","author":"PJ Robison","year":"1993","unstructured":"Robison, P.J., Staples, J.: Formalizing a hierarchical structure of practical mathematical reasoning. J. Logic Comput. 3(1), 47\u201361 (1993). \nhttp:\/\/dx.doi.org\/10.1093\/logcom\/3.1.47","journal-title":"J. Logic Comput."},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-642-27705-4_11","volume-title":"Verified Software: Theories, Tools, Experiments","author":"L Segal","year":"2012","unstructured":"Segal, L., Chalin, P.: A comparison of intermediate verification languages: Boogie and Sireum\/Pilar. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 130\u2013145. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-27705-4_11"},{"key":"5_CR29","unstructured":"The SMT-LIB standard: Version 2.0"},{"key":"5_CR30","unstructured":"The Whiley programming language. \nhttp:\/\/whiley.org"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66845-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:39:01Z","timestamp":1503747541000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}