{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T09:10:01Z","timestamp":1746177001655,"version":"3.40.4"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319054155"},{"type":"electronic","value":"9783319054162"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-05416-2_10","type":"book-chapter","created":{"date-parts":[[2014,4,5]],"date-time":"2014-04-05T05:41:09Z","timestamp":1396676469000},"page":"142-159","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Reflections on Verifying Software with Whiley"],"prefix":"10.1007","author":[{"given":"David J.","family":"Pearce","sequence":"first","affiliation":[]},{"given":"Lindsay","family":"Groves","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,4,6]]},"reference":[{"issue":"1","key":"10_CR1","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"CAR Hoare","year":"2003","unstructured":"Hoare, C.A.R.: The verifying compiler: a grand challenge for computing research. JACM 50(1), 63\u201369 (2003)","journal-title":"JACM"},{"key":"10_CR2","unstructured":"King, S.: A program verifier. Ph.D. thesis, Carnegie-Mellon University (1969)"},{"key":"10_CR3","unstructured":"Peter Deutsch, L.: An interactive program verifier. Ph.D. thesis, University of California (1973)"},{"key":"10_CR4","first-page":"55","volume-title":"Mathematical Logic and Programming Languages","author":"DI Good","year":"1985","unstructured":"Good, D.I.: Mechanical proofs about computer programs. In: Hoare, C.A.R., Shepherdson, J.C. (eds.) Mathematical Logic and Programming Languages, pp. 55\u201375. Prentice Hall, Englewood Cliffs (1985)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Luckham, D.C., German, S.M., von Henke, F.W., Karp, R.A., Milne, P.W., Oppen, D.C., Polak, W., Scherlis, W.L.: Stanford pascal verifier user manual. Technical report CS-TR-79-731, Department of Computer Science, Stanford University (1979)","DOI":"10.21236\/ADA071900"},{"key":"10_CR6","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":"10_CR7","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\/543552.512558"},{"issue":"1\u20133","key":"10_CR8","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.scico.2004.05.015","volume":"55","author":"GT Leavens","year":"2005","unstructured":"Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Sci. Comput. Program. 55(1\u20133), 185\u2013208 (2005)","journal-title":"Sci. Comput. Program."},{"key":"10_CR9","series-title":"LNCS","first-page":"108","volume-title":"CASSIS 2004","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)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Barnett, M., Rustan, K., Leino, M., Schulte, W.: The Spec# programming system: an overview. Technical report, Microsoft Research (2004)","DOI":"10.1007\/978-3-540-30569-9_3"},{"issue":"6","key":"10_CR11","doi-asserted-by":"publisher","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. J. Object Technol. 3(6), 27\u201356 (2004)","journal-title":"J. Object Technol."},{"key":"10_CR12","series-title":"LNCS","first-page":"364","volume-title":"FMCO 2006","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Evan Chang, B.-Y., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2006. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"10_CR13","series-title":"LNCS","first-page":"348","volume-title":"LPAR-16 2010","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-16 2010. LNCS, vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010)"},{"key":"10_CR14","series-title":"LNCS","first-page":"82","volume-title":"VSTTE 2012","author":"K Rustan","year":"2012","unstructured":"Rustan, K., Leino, M.: Developing verified programs with Dafny. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, p. 82. Springer, Heidelberg (2012)"},{"key":"10_CR15","unstructured":"The whiley programming language. http:\/\/whiley.org"},{"key":"10_CR16","series-title":"LNCS","first-page":"238","volume-title":"SLE 2013","author":"DJ Pearce","year":"2013","unstructured":"Pearce, D.J., Groves, L.: Whiley: a platform for research in software verification. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 238\u2013248. Springer, Heidelberg (2013)"},{"issue":"1","key":"10_CR17","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.entcs.2011.11.005","volume":"279","author":"D Pearce","year":"2011","unstructured":"Pearce, D., Noble, J.: Implementing a language with flow-sensitive and structural typing on the JVM. Electron. Notes Theoret. Comput. Sci. 279(1), 47\u201359 (2011)","journal-title":"Electron. Notes Theoret. Comput. Sci."},{"key":"10_CR18","series-title":"LNCS","first-page":"335","volume-title":"VMCAI 2013","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)"},{"key":"10_CR19","series-title":"LNCS","first-page":"358","volume-title":"TACAS 2007","author":"RE Bryant","year":"2007","unstructured":"Bryant, R.E., Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O., Brady, B.A.: Deciding bit-vector arithmetic with abstraction. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 358\u2013372. Springer, Heidelberg (2007)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Proceedings AMS, vol. 19, pp. 19\u201331. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"10_CR21","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12, 576\u2013580 (1969)","journal-title":"CACM"},{"key":"10_CR22","doi-asserted-by":"publisher","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":"10_CR23","doi-asserted-by":"crossref","unstructured":"Rountev, A.: Precise identification of side-effect-free methods in Java. In: Proceedings of ICSM, pp. 82\u201391. IEEE Computer Society (2004)","DOI":"10.1109\/ICSM.2004.1357793"},{"key":"10_CR24","series-title":"LNCS","first-page":"199","volume-title":"VMCAI 2005","author":"A S\u0103lcianu","year":"2005","unstructured":"S\u0103lcianu, A., Rinard, M.: Purity and side effect analysis for Java programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 199\u2013215. Springer, Heidelberg (2005)"},{"key":"10_CR25","series-title":"LNCS","first-page":"18","volume-title":"SAS 2007","author":"A Mycroft","year":"2007","unstructured":"Mycroft, A.: Programming language design and analysis motivated by hardware evolution. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 18\u201333. Springer, Heidelberg (2007)"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Tobin-Hochstadt, S., Felleisen, M.: Logical types for untyped languages. In: Proceedings of ICFP, pp. 117\u2013128 (2010)","DOI":"10.1145\/1932681.1863561"},{"key":"10_CR27","series-title":"LNCS","first-page":"256","volume-title":"ESOP 2011","author":"A Guha","year":"2011","unstructured":"Guha, A., Saftoiu, C., Krishnamurthi, S.: Typing local control and state using flow analysis. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 256\u2013275. Springer, Heidelberg (2011)"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Barbanera, F., Dezani-Cian Caglini, M.: Intersection and union types. In: Proceedings of the TACS, pp. 651\u2013674 (1991)","DOI":"10.1007\/3-540-54415-1_69"},{"issue":"2","key":"10_CR29","doi-asserted-by":"publisher","first-page":"31","DOI":"10.5381\/jot.2007.6.2.a3","volume":"6","author":"A Igarashi","year":"2007","unstructured":"Igarashi, A., Nagira, H.: Union types for object-oriented programming. J. Object Technol. 6(2), 31\u201352 (2007)","journal-title":"J. Object Technol."},{"key":"10_CR30","volume-title":"Types and Programming Languages","author":"BC Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"10_CR31","unstructured":"Hoare, T.: Null references: The billion dollar mistake, presentation at QCon (2009)"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: Proceedings of the OOPSLA, pp. 302\u2013312. ACM Press (2003)","DOI":"10.1145\/949343.949332"},{"issue":"9","key":"10_CR33","doi-asserted-by":"publisher","first-page":"455","DOI":"10.5381\/jot.2007.6.9.a23","volume":"6","author":"T Ekman","year":"2007","unstructured":"Ekman, T., Hedin, G.: Pluggable checking and inferencing of non-null types for Java. J. Object Technol. 6(9), 455\u2013475 (2007)","journal-title":"J. Object Technol."},{"key":"10_CR34","series-title":"LNCS","first-page":"227","volume-title":"ECOOP 2007","author":"P Chalin","year":"2007","unstructured":"Chalin, P., James, P.R.: Non-null references by default in Java: alleviating the nullity annotation burden. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 227\u2013247. Springer, Heidelberg (2007)"},{"key":"10_CR35","series-title":"LNCS","first-page":"229","volume-title":"CC 2008","author":"C Male","year":"2008","unstructured":"Male, C., Pearce, D.J., Potanin, A., Dymnikov, C.: Java bytecode verification for @NonNull types. In: Hendren, L. (ed.) CC 2008. LNCS, vol. 4959, pp. 229\u2013244. Springer, Heidelberg (2008)"},{"key":"10_CR36","doi-asserted-by":"crossref","unstructured":"Hubert, L.: A non-null annotation inference for Java bytecode. In: Proceedings of the PASTE, pp. 36\u201342. ACM (2008)","DOI":"10.1145\/1512475.1512484"},{"key":"10_CR37","unstructured":"ISO\/IEC. international standard ISO\/IEC 9899, programming languages \u2013 C (1990)"},{"key":"10_CR38","series-title":"LNCS","first-page":"22","volume-title":"CC 2011","author":"N Lameed","year":"2011","unstructured":"Lameed, N., Hendren, L.: Staged static techniques to efficiently implement array copy semantics in a MATLAB JIT compiler. In: Knoop, J. (ed.) CC 2011. LNCS, vol. 6601, pp. 22\u201341. Springer, Heidelberg (2011)"},{"issue":"3","key":"10_CR39","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1016\/j.cosrev.2011.02.002","volume":"5","author":"MJ Frade","year":"2011","unstructured":"Frade, M.J., Pinto, J.S.: Verification conditions for source-level imperative programs. Comput. Sci. Rev. 5(3), 252\u2013277 (2011)","journal-title":"Comput. Sci. Rev."},{"key":"10_CR40","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-1-84882-912-1_5","volume-title":"Reflections on the Work of C.A.R. Hoare, History of Computing","author":"M Gordon","year":"2010","unstructured":"Gordon, M., Collavizza, H.: Forward with Hoare. In: Roscoe, A.W., Jones, C.B., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare, History of Computing, pp. 101\u2013121. Springer, London (2010)"},{"issue":"5 & 6","key":"10_CR41","doi-asserted-by":"publisher","first-page":"705","DOI":"10.1016\/S0747-7171(06)80010-6","volume":"15","author":"R Chadha","year":"1993","unstructured":"Chadha, R., Plaisted, D.A.: On the mechanical derivation of loop invariants. J. Symbolic Comput. 15(5 & 6), 705\u2013744 (1993)","journal-title":"J. Symbolic Comput."},{"key":"10_CR42","series-title":"LNCS","first-page":"119","volume-title":"APLAS 2005","author":"KRM Leino","year":"2005","unstructured":"Leino, K.R.M., Logozzo, F.: Loop invariants on demand. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 119\u2013134. Springer, Heidelberg (2005)"},{"key":"10_CR43","unstructured":"Furia, C.A., Meyer, B.: Inferring loop invariants using postconditions. CoRR, abs\/0909.0884 (2009)"},{"key":"10_CR44","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proceedings of the TACAS, pp. 337\u2013340, (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"10_CR45","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"DL Detlefs","year":"2005","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. JACM 52, 365\u2013473 (2005)","journal-title":"JACM"},{"issue":"1\u20133","key":"10_CR46","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1016\/j.scico.2004.05.016","volume":"55","author":"KRM Leino","year":"2005","unstructured":"Leino, K.R.M., Millstein, T.D., Saxe, J.B.: Generating error traces from verification-condition counterexamples. Sci. Comput. Program. 55(1\u20133), 209\u2013226 (2005)","journal-title":"Sci. Comput. Program."},{"key":"10_CR47","unstructured":"Jager, I., Brumley, D.: Efficient directionless weakest preconditions. Technical Report CMU-CyLab-10-002, Carnegie Mellon University (2010)"},{"key":"10_CR48","series-title":"LNCS","first-page":"173","volume-title":"CAV 2007","author":"J-C Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"10_CR49","doi-asserted-by":"crossref","unstructured":"Barnett, M., Rustan M. Leino, K.: Weakest-precondition of unstructured programs. In: Proceedings of the PASTE, pp. 82\u201387. ACM Press (2005)","DOI":"10.1145\/1108768.1108813"},{"issue":"1\u20132","key":"10_CR50","first-page":"61","volume":"58","author":"B Jacobs","year":"2004","unstructured":"Jacobs, B.: Weakest pre-condition reasoning for Java programs with JML annotations. JLAP 58(1\u20132), 61\u201388 (2004)","journal-title":"JLAP"},{"key":"10_CR51","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003","author":"L Burdy","year":"2003","unstructured":"Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: a developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 422\u2013439. Springer, Heidelberg (2003)"},{"key":"10_CR52","doi-asserted-by":"crossref","unstructured":"Chandra, S., Fink, S.J., Sridharan, M.: Snugglebug: a powerful approach to weakest preconditions. In: Proceedings of the PLDI, pp. 363\u2013374. ACM Press (2009)","DOI":"10.1145\/1543135.1542517"},{"key":"10_CR53","series-title":"LNCS","first-page":"145","volume-title":"AMAST 2008","author":"E Denney","year":"2008","unstructured":"Denney, E., Fischer, B.: Explaining verification conditions. In: Meseguer, J., Ro\u015fu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 145\u2013159. Springer, Heidelberg (2008)"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-05416-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T08:47:00Z","timestamp":1746175620000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05416-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319054155","9783319054162"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05416-2_10","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"6 April 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}