{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:37:28Z","timestamp":1780115848604,"version":"3.54.0"},"publisher-location":"Cham","reference-count":58,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030176006","type":"print"},{"value":"9783030176013","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-17601-3_1","type":"book-chapter","created":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T19:20:54Z","timestamp":1555442454000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["An Introduction to Software Verification with Whiley"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4535-9677","authenticated-orcid":false,"given":"David J.","family":"Pearce","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3134-6306","authenticated-orcid":false,"given":"Mark","family":"Utting","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lindsay","family":"Groves","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,4,14]]},"reference":[{"key":"1_CR1","unstructured":"European Space Agency: Ariane 5: Flight 501 failure. Report by the Enquiry Board (1996)"},{"key":"1_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-77966-7_15","volume-title":"Hardware and Software: Verification and Testing","author":"D Babi\u0107","year":"2008","unstructured":"Babi\u0107, D., Hu, A.J.: Exploiting shared structure in software verification conditions. In: Yorav, K. (ed.) HVC 2007. LNCS, vol. 4899, pp. 169\u2013184. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-77966-7_15"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-540-73368-3_41","volume-title":"Computer Aided Verification","author":"D Babi\u0107","year":"2007","unstructured":"Babi\u0107, D., Hu, A.J.: Structural abstraction of software verification conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 366\u2013378. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_41"},{"key":"1_CR4","series-title":"Graduate Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Approach","author":"RJR Back","year":"1998","unstructured":"Back, R.J.R., von Wright, J.: Refinement Calculus: A Systematic Approach. Graduate Texts in Computer Science. Springer, New York (1998). https:\/\/doi.org\/10.1007\/978-1-4612-1674-2"},{"key":"1_CR5","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: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"issue":"6","key":"1_CR6","doi-asserted-by":"publisher","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. Commun. ACM 54(6), 81\u201391 (2011)","journal-title":"Commun. ACM"},{"issue":"6","key":"1_CR7","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":"1_CR8","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Proceedings of the Workshop on Program Analysis for Software Tools and Engineering (PASTE), pp. 82\u201387. ACM Press (2005)","DOI":"10.1145\/1108792.1108813"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-540-45236-2_24","volume-title":"FME 2003: Formal Methods","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). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_24"},{"issue":"4","key":"1_CR10","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1109\/MSP.2014.66","volume":"12","author":"M Carvalho","year":"2014","unstructured":"Carvalho, M., DeMott, J., Ford, R., Wheeler, D.: Heartbleed 101. IEEE Secur. Priv. 12(4), 63\u201367 (2014)","journal-title":"IEEE Secur. Priv."},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/3-540-45614-7_16","volume-title":"FME 2002:Formal Methods\u2014Getting IT Right","author":"N Cata\u00f1o","year":"2002","unstructured":"Cata\u00f1o, N., Huisman, M.: Formal specification and static checking of gemplus\u2019 electronic purse using ESC\/Java. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 272\u2013289. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45614-7_16"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-68237-0_18","volume-title":"FM 2008: Formal Methods","author":"P Chalin","year":"2008","unstructured":"Chalin, P., Rioux, F.: JML runtime assertion checking: improved error reporting and efficiency using strong validity. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 246\u2013261. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68237-0_18"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Chandra, S., Fink, S.J., Sridharan, M.: Snugglebug: a powerful approach to weakest preconditions. In: Proceedings of the ACM conference on Programming Language Design and Implementation (PLDI), pp. 363\u2013374. ACM Press (2009)","DOI":"10.1145\/1542476.1542517"},{"key":"1_CR14","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1109\/MSPEC.2009.5340234","volume":"46","author":"R Charette","year":"2009","unstructured":"Charette, R.: This car runs on code. IEEE Spectr. 46, 3 (2009)","journal-title":"IEEE Spectr."},{"issue":"9","key":"1_CR15","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/MSPEC.2005.1502528","volume":"42","author":"RN Charette","year":"2005","unstructured":"Charette, R.N.: Why software fails. IEEE Spect. 42(9), 42\u201349 (2005)","journal-title":"IEEE Spect."},{"key":"1_CR16","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., et al.: 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). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_2"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/978-3-642-20398-5_35","volume-title":"NASA Formal Methods","author":"DR Cok","year":"2011","unstructured":"Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472\u2013479. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_35"},{"key":"1_CR18","doi-asserted-by":"publisher","first-page":"79","DOI":"10.4204\/EPTCS.149.8","volume":"149","author":"David R. Cok","year":"2014","unstructured":"Cok, D.R.: OpenJML: Software verification for Java 7 using JML, OpenJDK, and eclipse. In: Proceedings of the Workshop on Formal Integrated Development Environment (F-IDE), vol. 149, pp. 79\u201392 (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Cytron, R., Ferrante, J., Rosen, B., Wegman, M., Zadeck, F.K.: An efficient method of computing static single assignment form. In: Proceedings of the ACM symposium on the Principles Of Programming Languages (POPL), pp. 25\u201335 (1989)","DOI":"10.1145\/75277.75280"},{"issue":"4","key":"1_CR20","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13(4), 451\u2013490 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-79980-1_12","volume-title":"Algebraic Methodology and Software Technology","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). https:\/\/doi.org\/10.1007\/978-3-540-79980-1_12"},{"issue":"3","key":"1_CR22","doi-asserted-by":"publisher","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. J. ACM 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"1_CR23","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":"1_CR24","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. Commun. ACM 18, 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Durumeric, Z., et al.: The matter of heartbleed. In: Proceedings of Internet Measurement Conference (IMC), pp. 475\u2013488. ACM Press (2014)","DOI":"10.1145\/2663716.2663755"},{"key":"1_CR26","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 ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pp. 302\u2013312. ACM Press (2003)","DOI":"10.1145\/949305.949332"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","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). https:\/\/doi.org\/10.1007\/978-3-540-73368-3_21"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the ACM conference on Programming Language Design and Implementation (PLDI), pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: Proceedings of the ACM symposium on the Principles Of Programming Languages (POPL), pp. 193\u2013205. ACM Press (2001)","DOI":"10.1145\/360204.360220"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Proceedings of Symposia in Applied Mathematics, vol. 19, pp. 19\u201331. American Mathematical Society (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"3","key":"1_CR31","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":"1_CR32","unstructured":"Software problem led to system failure at dhahran, saudi arabia, gao report #b-247094 (1992)"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Grigore, R., Charles, J., Fairmichael, F., Kiniry, J.: Strongest postcondition of unstructured programs. In: Proceedings of the Workshop on Formal Techniques for Java-like Programs (FTFJP), pp. 6:1\u20136:7. ACM Press (2009)","DOI":"10.1145\/1557898.1557904"},{"key":"1_CR34","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"},{"issue":"6","key":"1_CR35","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/MS.2015.147","volume":"32","author":"GJ Holzmann","year":"2015","unstructured":"Holzmann, G.J.: Out of bounds. IEEE Softw. 32(6), 24\u201326 (2015)","journal-title":"IEEE Softw."},{"key":"1_CR36","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: Verifythis verification competition 2012 - organizer\u2019s report (2013)"},{"issue":"1\u20132","key":"1_CR37","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.jlap.2003.07.005","volume":"58","author":"B Jacobs","year":"2004","unstructured":"Jacobs, B.: Weakest pre-condition reasoning for Java programs with JML annotations. J. Log. Algebr. Program. 58(1\u20132), 61\u201388 (2004)","journal-title":"J. Log. Algebr. Program."},{"key":"1_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11813040_19","volume-title":"FM 2006: Formal Methods","author":"IT Kassios","year":"2006","unstructured":"Kassios, I.T.: Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268\u2013283. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11813040_19"},{"key":"1_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-21437-0_14","volume-title":"FM 2011: Formal Methods","author":"V Klebanov","year":"2011","unstructured":"Klebanov, V., et al.: The 1st verified software competition: experience report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 154\u2013168. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_14"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Ko, A.J., Dosono, B., Duriseti, N.: Thirty years of software problems in the news. In: Proceedings of the 7th International Workshop on Cooperative and Human Aspects of Software Engineering, CHASE 2014, Hyderabad, India, 2\u20133 June 2014. ACM Press (2014)","DOI":"10.1145\/2593702.2593719"},{"issue":"1\u20133","key":"1_CR41","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."},{"issue":"6","key":"1_CR42","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"KRM Leino","year":"2005","unstructured":"Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6), 281\u2013288 (2005)","journal-title":"Inf. Process. Lett."},{"key":"1_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-642-27705-4_7","volume-title":"Verified Software: Theories, Tools, Experiments","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). https:\/\/doi.org\/10.1007\/978-3-642-27705-4_7"},{"key":"1_CR44","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). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"1_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-642-13010-6_4","volume-title":"Advanced Lectures on Software Engineering","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M., M\u00fcller, P.: Using the Spec# language, methodology, and tools to write bug-free programs. In: M\u00fcller, P. (ed.) LASER 2007\u20132008. LNCS, vol. 6029, pp. 91\u2013139. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13010-6_4"},{"key":"1_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-15057-9_8","volume-title":"Verified Software: Theories, Tools, Experiments","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M., Monahan, R.: Dafny meets the verification benchmarks challenge. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 112\u2013126. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15057-9_8"},{"issue":"7","key":"1_CR47","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/MC.1993.274940","volume":"26","author":"N Leveson","year":"1993","unstructured":"Leveson, N., Turner, C.: An investigation of the Therac-25 accidents. IEEE Comput. 26(7), 18\u201341 (1993)","journal-title":"IEEE Comput."},{"key":"1_CR48","volume-title":"Programming from Specifications","author":"C Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall, Upper Saddle River (1994)","edition":"2"},{"key":"1_CR49","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 de Moura","year":"2008","unstructured":"de 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). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"1_CR50","doi-asserted-by":"crossref","unstructured":"Pearce, D.J.: Integer range analysis for Whiley on embedded systems. In: Proceedings of the IEEE\/IFIP Workshop on Software Technologies for Future Embedded and Ubiquitous Systems, pp. 26\u201333 (2015)","DOI":"10.1109\/ISORCW.2015.54"},{"key":"1_CR51","unstructured":"Pearce, D.J.: The Whiley Language Specification (Updated, 2016)"},{"key":"1_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-319-02654-1_13","volume-title":"Software Language Engineering","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, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02654-1_13"},{"issue":"3","key":"1_CR53","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1504\/IJCIS.2009.024872","volume":"5","author":"HA Rahman","year":"2009","unstructured":"Rahman, H.A., Beznosov, K., Mart\u00ed, J.R.: Identification of sources of failures and their propagation in critical infrastructures from 12 years of public failure reports. Int. J. Crit. Infrastruct. 5(3), 220\u2013244 (2009)","journal-title":"Int. J. Crit. Infrastruct."},{"key":"1_CR54","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez, J., Leavens, G.T.: Static verification of PtolemyRely programs using OpenJML. In: Proceedings of the Workshop on Foundations of Aspect-Oriented Languages (FOAL), pp. 13\u201318. ACM Press (2014)","DOI":"10.1145\/2588548.2588550"},{"key":"1_CR55","unstructured":"Steinberg, J.: Massive internet security vulnerability - here\u2019s what you need to do (2014). https:\/\/www.forbes.com\/sites\/josephsteinberg\/2014\/04\/10\/massive-internet-security-vulnerability-you-are-at-risk-what-you-need-to-do. Accessed 12 Jan 2019"},{"key":"1_CR56","unstructured":"Stevens, M.: Demonstrating Whiley on an embedded system. Technical report, School of Engineering and Computer Science, Victoria University of Wellington (2014). http:\/\/www.ecs.vuw.ac.nz\/~djp\/files\/MattStevensENGR489.pdf"},{"key":"1_CR57","doi-asserted-by":"publisher","unstructured":"Weng, M.H., Pfahringer, B., Utting, M.: Static techniques for reducing memory usage in the C implementation of Whiley programs. In: Proceedings of the Australasian Computer Science Week Multiconference, ACSW 2017, pp. 15:1\u201315:8. ACM, New York (2017). https:\/\/doi.org\/10.1145\/3014812.3014827","DOI":"10.1145\/3014812.3014827"},{"issue":"9","key":"1_CR58","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.tej.2003.10.002","volume":"16","author":"D White","year":"2003","unstructured":"White, D., Roschelle, A., Peterson, P., Schlissel, D., Biewald, B., Steinhurst, W.: The 2003 blackout: solutions that won\u2019t cost a fortune. Electr. J. 16(9), 43\u201353 (2003)","journal-title":"Electr. J."}],"container-title":["Lecture Notes in Computer Science","Engineering Trustworthy Software Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17601-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T01:30:30Z","timestamp":1757295030000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-17601-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030176006","9783030176013"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17601-3_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"14 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Summer School on Engineering Trustworthy Software Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Chongqing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setss2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.swu-rise.net.cn\/SETSS2018\/SETSS2018.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Open","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"100% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1-2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1-2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}