{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:07Z","timestamp":1740123367503,"version":"3.37.3"},"reference-count":171,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,3,20]],"date-time":"2022-03-20T00:00:00Z","timestamp":1647734400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,20]],"date-time":"2022-03-20T00:00:00Z","timestamp":1647734400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001794","name":"The University of Queensland","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100001794","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2022,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The quest to develop increasingly sophisticated verification systems continues unabated. Tools such as Dafny, Spec#, ESC\/Java, SPARK Ada and Whiley attempt to seamlessly integrate specification and verification into a programming language, in a similar way to type checking. A common integration approach is to generate verification conditions that are handed off to an automated theorem prover. This provides a nice separation of concerns and allows different theorem provers to be used interchangeably. However, generating verification conditions is still a difficult undertaking and the use of more \u201chigh-level\u201d intermediate verification languages has become commonplace. In particular, Boogie provides a widely used and understood intermediate verification language. A common difficulty is the potential for an impedance mismatch between the source language and the intermediate verification language. In this paper, we explore the use of Boogie as an intermediate verification language for verifying programs in Whiley. This is noteworthy because the Whiley language has (amongst other things) a rich type system with considerable potential for an impedance mismatch. We provide a comprehensive account of translating Whiley to Boogie which demonstrates that it is possible to model most aspects of the Whiley language. Key challenges posed by the Whiley language included: the encoding of Whiley\u2019s expressive type system and support for flow typing and generics; the implicit assumption that expressions in specifications are well defined; the ability to invoke methods from within expressions; the ability to return multiple values from a function or method; the presence of unrestricted lambda functions; and the limited syntax for framing. We demonstrate that the resulting verification tool can verify significantly more programs than the native Whiley verifier which was custom-built for Whiley verification. Furthermore, our work provides evidence that Boogie is (for the most part) sufficiently general to act as an intermediate language for a wide range of source languages.<\/jats:p>","DOI":"10.1007\/s10817-022-09619-1","type":"journal-article","created":{"date-parts":[[2022,3,20]],"date-time":"2022-03-20T15:02:43Z","timestamp":1647788563000},"page":"747-803","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying Whiley Programs with Boogie"],"prefix":"10.1007","volume":"66","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4535-9677","authenticated-orcid":false,"given":"David J.","family":"Pearce","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3134-6306","authenticated-orcid":false,"given":"Mark","family":"Utting","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9179-3602","authenticated-orcid":false,"given":"Lindsay","family":"Groves","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,20]]},"reference":[{"key":"9619_CR1","doi-asserted-by":"crossref","unstructured":"Ahmadi, R., Leino, K.R.M., Nummenmaa, J.: Automatic verification of Dafny programs with traits. In: Proceedings of the Workshop on Formal Techniques for Java-like Programs (FTFJP), pp. 4:1\u20134:5. ACM Press (2015)","DOI":"10.1145\/2786536.2786542"},{"key":"9619_CR2","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification\u2014The KeY Book\u2014From Theory to Practice, LNCS, vol. 10001. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"9619_CR3","doi-asserted-by":"crossref","unstructured":"Altidor, J., Huang, S.S., Smaragdakis, Y.: Taming the wildcards: combining definition- and use-site variance. In: Proceedings of the ACM conference on Programming Language Design and Implementation (PLDI), pp. 602\u2013613. ACM Press (2011)","DOI":"10.1145\/1993316.1993569"},{"key":"9619_CR4","doi-asserted-by":"crossref","unstructured":"Ameri, M., Furia, C.A.: Why just Boogie? Translating between intermediate verification languages. In: Proceedings of the Conference on Integrated Formal Methods (iFM), pp. 79\u201395 (2016)","DOI":"10.1007\/978-3-319-33693-0_6"},{"key":"9619_CR5","doi-asserted-by":"crossref","unstructured":"Amighi, A., Blom, S., Darabi, S., Huisman, M., Mostowski, W., Zaharieva-Stojanovski, M.: Verification of concurrent systems with VerCors. In: International School on Formal Methods (SFM), LNCS, vol. 8483, pp. 172\u2013216. Springer-Verlag (2014)","DOI":"10.1007\/978-3-319-07317-0_5"},{"key":"9619_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics\u2014for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W.: Program Logics\u2014for Certified Compilers. Cambridge University Press, Cambridge (2014)"},{"key":"9619_CR7","doi-asserted-by":"crossref","unstructured":"Arlt, S., R\u00fcmmer, P., Sch\u00e4f, M.: Joogie: from Java through Jimple to Boogie. In: Proceedings of the Workshop on State of the Art in Java Program analysis (2013)","DOI":"10.1145\/2487568.2487570"},{"key":"9619_CR8","doi-asserted-by":"crossref","unstructured":"Astrauskas, V., M\u00fcller, P., Poli, F., Summers, A.J.: Leveraging Rust types for modular specification and verification. In: Proceedings of the ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), p. Article 147. ACM Press (2019)","DOI":"10.1145\/3360573"},{"key":"9619_CR9","doi-asserted-by":"publisher","unstructured":"Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional logic for local reasoning about global invariants. In: Proceedings of the European Conference on Object-Oriented Programming (ECOOP), pp. 387\u2013411. Springer-Verlag (2008). https:\/\/doi.org\/10.1007\/978-3-540-70592-5_17","DOI":"10.1007\/978-3-540-70592-5_17"},{"issue":"1","key":"9619_CR10","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/j.entcs.2005.02.026","volume":"141","author":"F Bannwart","year":"2005","unstructured":"Bannwart, F., M\u00fcller, P.: A program logic for bytecode. Electron. Notes Comput. Sci. 141(1), 255\u2013273 (2005)","journal-title":"Electron. Notes Comput. Sci."},{"key":"9619_CR11","doi-asserted-by":"crossref","unstructured":"Baranowski, M., He, S., Rakamari\u0107, Z.: Verifying Rust programs with SMACK. In: Automated Technology for Verification and Analysis, pp. 528\u2013535. Springer-Verlag (2018)","DOI":"10.1007\/978-3-030-01090-4_32"},{"key":"9619_CR12","doi-asserted-by":"crossref","unstructured":"Barbanera, F., Caglini, M.D.C.: Intersection and union types. In: Proceedings of the Conference on Theoretical Aspects of Computer Software (TACS), pp. 651\u2013674 (1991)","DOI":"10.1007\/3-540-54415-1_69"},{"key":"9619_CR13","unstructured":"Barnes, J.: High Integrity Ada: The SPARK Approach. Addison Wesley Longman, Inc., Reading (1997)"},{"key":"9619_CR14","doi-asserted-by":"crossref","unstructured":"Barnett, M., Chang, B.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: Proceedings of the Formal Methods for Components and Objects (FMCO), pp. 364\u2013387 (2006)","DOI":"10.1007\/11804192_17"},{"issue":"6","key":"9619_CR15","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."},{"issue":"6","key":"9619_CR16","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"},{"key":"9619_CR17","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\/1108768.1108813"},{"key":"9619_CR18","doi-asserted-by":"crossref","unstructured":"Barnett, M., Leino, K.R.M.: To goto where no statement has gone before. In: Proceedings of the Conference on Verified Software: Theories, Tools, Experiments (VSTTE), LNCS, vol. 6217, pp. 157\u2013168. Springer-Verlag (2010)","DOI":"10.1007\/978-3-642-15057-9_11"},{"key":"9619_CR19","doi-asserted-by":"crossref","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Proceedings of Conference on Computer Aided Verification (CAV), pp. 298\u2013302 (2007)","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"9619_CR20","doi-asserted-by":"crossref","unstructured":"Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Proceedings of Conference on Computer Aided Verification (CAV), LNCS, vol. 6806, pp. 171\u2013177. Springer-Verlag (2011)","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"9619_CR21","unstructured":"Barrett, C.W., Stump, A., Tinelli, C.: The SMT-LIB standard version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, Scotland, (SMT \u201910) (2010)"},{"key":"9619_CR22","unstructured":"Baudin, P., Cuo, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C specification language (version 1.8)"},{"issue":"3","key":"9619_CR23","doi-asserted-by":"publisher","first-page":"22:1","DOI":"10.1145\/3319396","volume":"66","author":"P Beame","year":"2019","unstructured":"Beame, P., Liew, V.: Toward verifying nonlinear integer arithmetic. J. ACM 66(3), 22:1-22:30 (2019)","journal-title":"J. ACM"},{"key":"9619_CR24","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer-Verlag (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9619_CR25","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 ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pp. 113\u2013132. ACM Press (2012)","DOI":"10.1145\/2398857.2384625"},{"key":"9619_CR26","doi-asserted-by":"crossref","unstructured":"Blanchard, A., Kosmatov, N., Loulergue, F.: A lesson on verification of IoT software with Frama-C. In: Proceedings of the Conference on High Performance Computing & Simulation (HPCS), pp. 21\u201330. IEEE (2018)","DOI":"10.1109\/HPCS.2018.00018"},{"key":"9619_CR27","doi-asserted-by":"crossref","unstructured":"Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Proceedings of the Symposium on Formal Methods (FM), vol. 8442, pp. 127\u2013131. Springer-Verlag (2014)","DOI":"10.1007\/978-3-319-06410-9_9"},{"key":"9619_CR28","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":"9619_CR29","doi-asserted-by":"crossref","unstructured":"Boerman, J., Huisman, M., Joosten, S.J.C.: Reasoning about JML: Differences between KeY and OpenJML. In: Proceedings of the Conference on Integrated Formal Methods (iFM), LNCS, vol. 11023, pp. 30\u201346. Springer-Verlag (2018)","DOI":"10.1007\/978-3-319-98938-9_3"},{"key":"9619_CR30","doi-asserted-by":"crossref","unstructured":"Bornat, R.: Proving pointer programs in Hoare logic. In: Proceedings of the Conference on the Mathematics of Program Construction (MPC) (2000)","DOI":"10.1007\/10722010_8"},{"key":"9619_CR31","doi-asserted-by":"crossref","unstructured":"Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.C.: Using first-order theorem provers in the Jahob data structure verification system. In: Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 74\u201388 (2007)","DOI":"10.1007\/978-3-540-69738-1_5"},{"key":"9619_CR32","doi-asserted-by":"publisher","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), pp. 123\u2013133 (2002). https:\/\/doi.org\/10.1145\/566171.566191","DOI":"10.1145\/566171.566191"},{"key":"9619_CR33","doi-asserted-by":"crossref","unstructured":"Brandon, C., Chapin, P.: A SPARK\/Ada cubesat control program. In: Proceedings of the Conference on Reliable Software Technologies (RST), pp. 51\u201364 (2013)","DOI":"10.1007\/978-3-642-38601-5_4"},{"key":"9619_CR34","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/S1571-0661(04)80810-7","volume":"80","author":"L Burdy","year":"2003","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Electron. Notes Comput. Sci. 80, 75\u201391 (2003)","journal-title":"Electron. Notes Comput. Sci."},{"key":"9619_CR35","unstructured":"Cadar, C., Dunbar, D., Engler, D.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the Conference on Operating Systems Design and Implementation (OSDI), pp. 209\u2013224 (2008)"},{"key":"9619_CR36","doi-asserted-by":"crossref","unstructured":"Cardelli, L.: Structural subtyping and the notion of power type. In: Proceedings of the ACM Symposium on the Principles of Programming Languages (POPL), pp. 70\u201379. ACM Press (1988)","DOI":"10.1145\/73560.73566"},{"key":"9619_CR37","doi-asserted-by":"crossref","unstructured":"Cata\u00f1o, N., Huisman, M.: Formal specification and static checking of Gemplus\u2019 electronic purse using ESC\/Java. In: Proceedings of the Symposium on Formal Methods Europe (FME), LNCS, vol. 2391, pp. 272\u2013289. Springer-Verlag (2002)","DOI":"10.1007\/3-540-45614-7_16"},{"key":"9619_CR38","doi-asserted-by":"crossref","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC\/Java2. In: Proceedings of the Formal Methods for Components and Objects (FMCO), pp. 342\u2013363 (2005)","DOI":"10.1007\/11804192_16"},{"key":"9619_CR39","doi-asserted-by":"crossref","unstructured":"Chalin, P., Rioux, F.: JML runtime assertion checking: Improved error reporting and efficiency using strong validity. In: Proceedings of the Symposium on Formal Methods (FM), LNCS, vol. 5014, pp. 246\u2013261. Springer-Verlag (2008)","DOI":"10.1007\/978-3-540-68237-0_18"},{"key":"9619_CR40","doi-asserted-by":"crossref","unstructured":"Chapman, R., Schanda, F.: Are we there yet? 20 years of industrial theorem proving with SPARK. In: Proceedings of the Conference on Interactive Theorem Proving (ITP), pp. 17\u201326 (2014)","DOI":"10.1007\/978-3-319-08970-6_2"},{"key":"9619_CR41","doi-asserted-by":"crossref","unstructured":"Chen, Y., Furia, C.A.: Robustness testing of intermediate verifiers. In: Proceedings of the Conference on Automated Technology for Verification and Analysis (ATVA), LNCS, vol. 11138, pp. 91\u2013108. Springer (2018)","DOI":"10.1007\/978-3-030-01090-4_6"},{"key":"9619_CR42","doi-asserted-by":"publisher","unstructured":"Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: The JML and JUnit way. In: Proceedings of the European Conference on Object-Oriented Programming (ECOOP), pp. 231\u2013255. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-47993-7_10","DOI":"10.1007\/3-540-47993-7_10"},{"key":"9619_CR43","doi-asserted-by":"crossref","unstructured":"Chin, J., Pearce, D.J.: Finding bugs with specification-based testing is easy! The Art, Science, and Engineering of Programming 5, Article 13 (2021)","DOI":"10.22152\/programming-journal.org\/2021\/5\/13"},{"key":"9619_CR44","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Experimenting on solving nonlinear integer arithmetic with incremental linearization. In: Proceedings of Conference on Theory and Applications of Satisfiability Testing (SAT), LNCS, vol. 10929, pp. 383\u2013398. Springer-Verlag (2018)","DOI":"10.1007\/978-3-319-94144-8_23"},{"key":"9619_CR45","doi-asserted-by":"crossref","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: Proceedings of the Conference on Theorem Proving in Higher Order Logics (TPHOL), LNCS, vol. 5674, pp. 23\u201342. Springer-Verlag (2009)","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"9619_CR46","doi-asserted-by":"crossref","unstructured":"Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Proceedings of the NASA Formal Methods Symposium, LNCS, vol. 6617, pp. 472\u2013479. Springer-Verlag (2011)","DOI":"10.1007\/978-3-642-20398-5_35"},{"key":"9619_CR47","doi-asserted-by":"crossref","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)","DOI":"10.4204\/EPTCS.149.8"},{"key":"9619_CR48","doi-asserted-by":"crossref","unstructured":"Cok, D.R., Kiniry, J.: ESC\/Java2: Uniting ESC\/Java and JML. In: Proceedings of the Conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS), pp. 108\u2013128 (2005)","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"9619_CR49","unstructured":"Conchon, S., Coquereau, A., Iguernlala, M., Mebsout, A.: Alt-ergo 2.2. In: Workshop on Satisfiability Modulo Theories (SMT). HAL CCSD (2018)"},{"key":"9619_CR50","doi-asserted-by":"crossref","unstructured":"Cook, B., Kroening, D., Sharygina, N.: Accurate theorem proving for program verification. In: Proceedings of the Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), pp. 96\u2013114 (2004)","DOI":"10.1007\/11925040_7"},{"key":"9619_CR51","doi-asserted-by":"crossref","unstructured":"Corzilius, F., Loup, U., Junges, S., \u00c1brah\u00e1m, E.: SMT-RAT: An SMT-compliant nonlinear real arithmetic toolbox - (tool presentation). In: Proceedings of Conference on Theory and Applications of Satisfiability Testing (SAT), LNCS, vol. 7317, pp. 442\u2013448. Springer-Verlag (2012)","DOI":"10.1007\/978-3-642-31612-8_35"},{"key":"9619_CR52","doi-asserted-by":"crossref","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. In: Proceedings of the Conference on Software Engineering and Formal Methods (SEFM), LNCS, vol. 7504, pp. 233\u2013247. Springer-Verlag (2012)","DOI":"10.1007\/978-3-642-33826-7_16"},{"key":"9619_CR53","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proceedings of the conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9619_CR54","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. In: Proceedings of the Conference on Automated Deduction (CADE), pp. 183\u2013198 (2007)","DOI":"10.1007\/978-3-540-73595-3_13"},{"issue":"3","key":"9619_CR55","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":"9619_CR56","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":"9619_CR57","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":"9619_CR58","unstructured":"Dross, C., Efstathopoulos, P., Lesens, D., Mentr\u00e9, D., Moy, Y.: Rail, space, security: three case studies for spark 2014. In: Proceedings of the Congress on Embedded Real Time Systems (ERTS) (2014)"},{"key":"9619_CR59","doi-asserted-by":"crossref","unstructured":"Dross, C., Furia, C.A., Huisman, M., Monahan, R., M\u00fcller, P.: VerifyThis 2019: A program verification competition (extended report). CoRR arXiv:2008.13610 (2020)","DOI":"10.1007\/s10009-021-00619-x"},{"key":"9619_CR60","doi-asserted-by":"crossref","unstructured":"Dubochet, G., Odersky, M.: Compiling structural types on the JVM: a comparison of reflective and generative techniques from scala\u2019s perspective. In: Proceedings of the Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems Workshop (ICOOOLPS), pp. 34\u201341. ACM Press (2009)","DOI":"10.1145\/1565824.1565829"},{"key":"9619_CR61","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: Proceedings of Conference on Computer Aided Verification (CAV), LNCS, vol. 8559, pp. 737\u2013744. Springer-Verlag (2014)","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"9619_CR62","doi-asserted-by":"crossref","unstructured":"Dutertre, B., de\u00a0Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Proceedings of Conference on Computer Aided Verification (CAV), pp. 81\u201394 (2006)","DOI":"10.1007\/11817963_11"},{"key":"9619_CR63","doi-asserted-by":"crossref","unstructured":"Eilers, M., M\u00fcller, P.: Nagini: A static verifier for Python. In: Proceedings of Conference on Computer Aided Verification (CAV), LNCS, vol. 10981, pp. 596\u2013603. Springer-Verlag (2018)","DOI":"10.1007\/978-3-319-96145-3_33"},{"key":"9619_CR64","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\/949343.949332"},{"key":"9619_CR65","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J., Paskevich, A.: Why3\u2014where programs meet provers. In: Proceedings of the European Symposium on Programming (ESOP), pp. 125\u2013128 (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"9619_CR66","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C.: Verifying two lines of C with Why3: An exercise in program verification. In: Proceedings of the Conference on Verified Software: Theories, Tools, Experiments (VSTTE), LNCS, vol. 7152, pp. 83\u201397. Springer-Verlag (2012)","DOI":"10.1007\/978-3-642-27705-4_8"},{"key":"9619_CR67","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Proceedings of Conference on Computer Aided Verification (CAV), LNCS, vol. 4590, pp. 173\u2013177. Springer-Verlag (2007)","DOI":"10.1007\/978-3-540-73368-3_21"},{"key":"9619_CR68","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 the ACM conference on Programming Language Design and Implementation (PLDI), pp. 234\u2013245 (2002)","DOI":"10.1145\/543552.512558"},{"key":"9619_CR69","doi-asserted-by":"crossref","unstructured":"Furia, C.A., Poskitt, C.M., Tschannen, J.: The AutoProof verifier: usability by non-experts and on standard code. In: Proceedings of the Workshop on Formal Integrated Development Environment (F-IDE) (2015)","DOI":"10.4204\/EPTCS.187.4"},{"key":"9619_CR70","doi-asserted-by":"crossref","unstructured":"Games, M.: The fantastic combinations of John Conway\u2019s new solitaire game \u201clife\u201d by Martin Gardner. Scientific American 223, 120\u2013123 (1970)","DOI":"10.1038\/scientificamerican1070-120"},{"key":"9619_CR71","doi-asserted-by":"crossref","unstructured":"Ge, Y., de\u00a0Moura, L.M.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Proceedings of Conference on Computer Aided Verification (CAV), pp. 306\u2013320 (2009)","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"9619_CR72","doi-asserted-by":"crossref","unstructured":"Gil, J., Maman, I.: Whiteoak: introducing structural typing into Java. In: Proceedings of the ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pp. 73\u201390. ACM Press (2008)","DOI":"10.1145\/1449955.1449771"},{"key":"9619_CR73","doi-asserted-by":"crossref","unstructured":"Goodloe, A.E., Mu\u00f1oz, C., Kirchner, F., Correnson, L.: Verification of numerical programs: From real numbers to floating point numbers. In: Proceedings of the NASA Formal Methods Symposium, LNCS, vol. 7871, pp. 441\u2013446. Springer-Verlag (2013)","DOI":"10.1007\/978-3-642-38088-4_31"},{"key":"9619_CR74","doi-asserted-by":"crossref","unstructured":"Goues, C.L., Leino, K.R.M., Moskal, M.: The Boogie Verification Debugger (tool paper). In: Proceedings of the Conference on Software Engineering and Formal Methods (SEFM), LNCS, vol. 7041, pp. 407\u2013414. Springer-Verlag (2011)","DOI":"10.1007\/978-3-642-24690-6_28"},{"key":"9619_CR75","doi-asserted-by":"crossref","unstructured":"Gries, D.: The multiple assignment statement. IEEE Trans. Softw. Eng. 4, 89\u201393 (1978)","DOI":"10.1109\/TSE.1978.231479"},{"key":"9619_CR76","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5983-1","volume-title":"The Science of Programming","author":"D Gries","year":"1981","unstructured":"Gries, D.: The Science of Programming. Springer-Verlag, Berlin (1981)"},{"key":"9619_CR77","doi-asserted-by":"crossref","unstructured":"Guha, A., Saftoiu, C., Krishnamurthi, S.: Typing local control and state using flow analysis. In: Proceedings of the European Symposium on Programming (ESOP), pp. 256\u2013275 (2011)","DOI":"10.1007\/978-3-642-19718-5_14"},{"key":"9619_CR78","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Tiwari, A.: Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In: Proceedings of the European Symposium on Programming (ESOP), vol. 3924, pp. 279\u2013293 (2006)","DOI":"10.1007\/11693024_19"},{"key":"9619_CR79","doi-asserted-by":"crossref","unstructured":"Heule, S., Kassios, I.T., M\u00fcller, P., Summers, A.J.: Verification condition generation for permission logics with abstract predicates and abstraction functions. In: Proceedings of the European Conference on Object-Oriented Programming (ECOOP), pp. 451\u2013476 (2013)","DOI":"10.1007\/978-3-642-39038-8_19"},{"issue":"1","key":"9619_CR80","doi-asserted-by":"publisher","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. J. ACM 50(1), 63\u201369 (2003)","journal-title":"J. ACM"},{"key":"9619_CR81","doi-asserted-by":"crossref","unstructured":"Hocking, A.B., Knight, J.C., Aiello, M.A., Shiraishi, S.: Arguing software compliance with ISO 26262. In: Proceedings of the Symposium on Software Reliability Engineering (ISSRE), pp. 226\u2013231. IEEE Computer Society (2014)","DOI":"10.1109\/ISSREW.2014.88"},{"key":"9619_CR82","doi-asserted-by":"crossref","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Invariant generation in Vampire. In: Proceedings of the conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 6605, pp. 60\u201364. Springer-Verlag (2011)","DOI":"10.1007\/978-3-642-19835-9_7"},{"key":"9619_CR83","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis verification competition 2016\u2014organizer\u2019s report (2013)"},{"key":"9619_CR84","doi-asserted-by":"crossref","unstructured":"Igarashi, A., Nagira, H.: Union types for object-oriented programming. J. Obj. Technol. 6(2) (2007)","DOI":"10.5381\/jot.2007.6.2.a3"},{"key":"9619_CR85","doi-asserted-by":"crossref","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: Proceedings of the NASA Formal Methods Symposium, pp. 41\u201355 (2011)","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"9619_CR86","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS), pp. 304\u2013311 (2010)","DOI":"10.1007\/978-3-642-17164-2_21"},{"issue":"Supplement","key":"9619_CR87","first-page":"121","volume":"9","author":"TJ Jennings","year":"1989","unstructured":"Jennings, T.J., Carr\u00e9, B.A.: A subset of Ada for formal verification (SPARK). Ada User 9(Supplement), 121\u2013126 (1989)","journal-title":"Ada User"},{"key":"9619_CR88","doi-asserted-by":"crossref","unstructured":"Jovanovic, D.: Solving nonlinear integer arithmetic with MCSAT. In: Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS, vol. 10145, pp. 330\u2013346. Springer-Verlag (2017)","DOI":"10.1007\/978-3-319-52234-0_18"},{"key":"9619_CR89","doi-asserted-by":"crossref","unstructured":"Jung, R., Dang, H.H., Kang, J., Dreyer, D.: Stacked borrows: An aliasing model for Rust. In: Proceedings of the ACM symposium on the Principles Of Programming Languages (POPL), p. Article 41 (2020)","DOI":"10.1145\/3371109"},{"key":"9619_CR90","doi-asserted-by":"crossref","unstructured":"Jung, R., Jourdan, J.H., Krebbers, R., Dreyer, D.: RustBelt: Securing the foundations of the Rust programming language. In: Proceedings of the ACM Symposium on the Principles Of Programming Languages (POPL), pp. 66:1\u201366:34. ACM Press (2018)","DOI":"10.1145\/3158154"},{"key":"9619_CR91","doi-asserted-by":"crossref","unstructured":"Kassios, I.T.: Dynamic frames: Support for framing, dependencies and sharing without restrictions. In: Proceedings of the Symposium on Formal Methods (FM), LNCS, vol. 4085, pp. 268\u2013283. Springer-Verlag (2006)","DOI":"10.1007\/11813040_19"},{"key":"9619_CR92","unstructured":"Kassios, I.T.: Dynamic frames and automated verification. Tech. Rep. Tutorial for the. 2nd COST Action IC0701 Training School (2011)"},{"key":"9619_CR93","doi-asserted-by":"crossref","unstructured":"Klebanov, V., M\u00fcller, P., Shankar, N., Leavens, G.T., W\u00fcstholz, V., Alkassar, E., Arthan, R., Bronish, D., Chapman, R., Cohen, E., Hillebrand, M., Jacobs, B., Leino, K.R.M., Monahan, R., Piessens, F., Polikarpova, N., Ridge, T., Smans, J., Tobies, S., Tuerk, T., Ulbrich, M., Wei\u00df, B.: The 1st verified software competition: Experience report (VSComp). In: Proceedings of the Symposium on Formal Methods (FM), LNCS. Springer-Verlag (2011)","DOI":"10.1007\/978-3-642-21437-0_14"},{"key":"9619_CR94","doi-asserted-by":"crossref","unstructured":"Kosmatov, N., Signoles, J.: A lesson on runtime assertion checking with Frama-C. In: Proceedings of the Conference on Runtime Verification (RV), LNCS, vol. 8174, pp. 386\u2013399. Springer-Verlag (2013)","DOI":"10.1007\/978-3-642-40787-1_29"},{"key":"9619_CR95","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Proceedings of Conference on Computer Aided Verification (CAV), LNCS, vol. 8044, pp. 1\u201335. Springer-Verlag (2013)","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"9619_CR96","doi-asserted-by":"crossref","unstructured":"Kremer, G., Corzilius, F., \u00c1brah\u00e1m, E.: A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic. In: Computer Algebra in Scientific Computing (CASC), LNCS, vol. 9890, pp. 315\u2013335. Springer-Verlag (2016)","DOI":"10.1007\/978-3-319-45641-6_21"},{"key":"9619_CR97","doi-asserted-by":"crossref","unstructured":"Kroening, D., Tautschnig, M.: CBMC - C Bounded Model Checker. In: Proceedings of the conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 8413, pp. 389\u2013391. Springer-Verlag (2014)","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"9619_CR98","doi-asserted-by":"crossref","unstructured":"Lameed, N., Hendren, L.J.: Staged static techniques to efficiently implement array copy semantics in a MATLAB JIT compiler. In: Proceedings of the Confererence on Compiler Construction (CC), pp. 22\u201341 (2011)","DOI":"10.1007\/978-3-642-19861-8_3"},{"issue":"1\u20133","key":"9619_CR99","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":"9619_CR100","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)"},{"issue":"6","key":"9619_CR101","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":"9619_CR102","unstructured":"Leino, K.R.M.: Specification and verification of object-oriented software. Technical Report, Marktoberdorf Internation Summer School (2008)"},{"key":"9619_CR103","unstructured":"Leino, K.R.M.: This is Boogie 2 (2008). https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/. Microsoft Research, Manuscript KRML 178"},{"key":"9619_CR104","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Proceedings of the Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS, vol. 6355, pp. 348\u2013370. Springer-Verlag (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"9619_CR105","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Leino, K.R.M.: Developing verified programs with Dafny. In: Proceedings of the Conference on Verified Software: Theories, Tools, Experiments (VSTTE), LNCS, vol. 7152, pp. 82. Springer-Verlag (2012)","DOI":"10.1007\/978-3-642-27705-4_7"},{"key":"9619_CR106","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Program proving using intermediate verification languages (IVLs) like Boogie and Why3. In: Proceedings of the Workshop on Safe Languages and Technologies for Structured and Efficient Parallel and Distributed\/Cloud Computing (HILT), pp. 25\u201326 (2012)","DOI":"10.1145\/2402709.2402689"},{"key":"9619_CR107","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: Proceedings of the Symposium on Applied Computing (SAC), pp. 615\u2013622 (2009)","DOI":"10.1145\/1529282.1529411"},{"key":"9619_CR108","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Dafny meets the verification benchmarks challenge. In: Proceedings of the Conference on Verified Software: Theories, Tools, Experiments (VSTTE) LNCS, vol. 6217, pp. 112\u2013126. Springer-Verlag (2010)","DOI":"10.1007\/978-3-642-15057-9_8"},{"key":"9619_CR109","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., M\u00fcller, P.: Using the Spec# language, methodology, and tools to write bug-free programs. In: LASER Summer School, LNCS, vol. 6029, pp. 91\u2013139. Springer-Verlag (2008)","DOI":"10.1007\/978-3-642-13010-6_4"},{"key":"9619_CR110","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., M\u00fcller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Foundations of Security Analysis and Design V (FOSAD), pp. 195\u2013222 (2009)","DOI":"10.1007\/978-3-642-03829-7_7"},{"key":"9619_CR111","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Pit-Claudel, C.: Trigger selection strategies to stabilize program verifiers. In: Proceedings of Conference on Computer Aided Verification (CAV), LNCS, vol. 9779, pp. 361\u2013381. Springer-Verlag (2016)","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"9619_CR112","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: A polymorphic intermediate verification language: Design and logical encoding. In: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 6015, pp. 312\u2013327. Springer-Verlag (2010)","DOI":"10.1007\/978-3-642-12002-2_26"},{"key":"9619_CR113","unstructured":"Leino, K.R.M., Schulte, W.: A verifying compiler for a multi-threaded object-oriented language. In: Summer School Marktoberdorf 2006: Software System Reliability and Security, NATO ASI Series F. IOS Press, Amsterdam (2007)"},{"key":"9619_CR114","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Yessenov, K.: Stepwise refinement of heap-manipulating code in chalice. Formal Aspects of Computing 24(4-6) (2012)","DOI":"10.1007\/s00165-012-0254-3"},{"key":"9619_CR115","doi-asserted-by":"crossref","unstructured":"Lindner, M., Aparicius, J., Lindgren, P.: No panic! verification of Rust programs by symbolic execution. In: International Conference on Industrial Informatics (INDIN), pp. 108\u2013114 (2018)","DOI":"10.1109\/INDIN.2018.8471992"},{"key":"9619_CR116","doi-asserted-by":"crossref","unstructured":"Lindner, M., Fitinghoff, N., Eriksson, J., Lindgren, P.: Verification of safety functions implemented in Rust - a symbolic execution based approach. In: International Conference on Industrial Informatics (INDIN), vol.\u00a01, pp. 432\u2013439 (2019)","DOI":"10.1109\/INDIN41052.2019.8972014"},{"key":"9619_CR117","doi-asserted-by":"crossref","unstructured":"Malayeri, D., Aldrich, J.: Integrating nominal and structural subtyping. In: Proceedings of the European Conference on Object-Oriented Programming (ECOOP), pp. 260\u2013284 (2008)","DOI":"10.1007\/978-3-540-70592-5_12"},{"key":"9619_CR118","doi-asserted-by":"crossref","unstructured":"Malayeri, D., Aldrich, J.: Is structural subtyping useful? An empirical study. In: Proceedings of the European Symposium on Programming (ESOP), LNCS, vol. 5502, pp. 95\u2013111. Springer-Verlag (2009)","DOI":"10.1007\/978-3-642-00590-9_8"},{"key":"9619_CR119","doi-asserted-by":"crossref","unstructured":"Mangano, F., Duquennoy, S., Kosmatov, N.: Formal verification of a memory allocation module of contiki with Frama-C: a case study. In: Proceedings of the Conference on Software Engineering and Formal Methods (SEFM), pp. 114\u2013120. Springer-Verlag (2016)","DOI":"10.1007\/978-3-319-54876-0_9"},{"key":"9619_CR120","doi-asserted-by":"crossref","unstructured":"Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for Rust programs. In: Programming Languages and Systems, pp. 484\u2013514. Springer-Verlag (2020)","DOI":"10.1007\/978-3-030-44914-8_18"},{"key":"9619_CR121","doi-asserted-by":"publisher","unstructured":"McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press (2015). https:\/\/doi.org\/10.1017\/CBO9781139629294","DOI":"10.1017\/CBO9781139629294"},{"issue":"3","key":"9619_CR122","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0164-1212(88)90022-2","volume":"8","author":"B Meyer","year":"1988","unstructured":"Meyer, B.: Eiffel: a language and environment for software engineering. J. Syst. Softw. 8(3), 199\u2013246 (1988)","journal-title":"J. Syst. Softw."},{"key":"9619_CR123","doi-asserted-by":"crossref","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. IEEE. Comput. 25(10), 40\u201351 (1992)","DOI":"10.1109\/2.161279"},{"key":"9619_CR124","unstructured":"M\u00fchlberg1and, J.T., Freitas, L.: Verifying freertos: from requirements to binary code. In: Proceedings of the Workshop on Automated Verification of Critical Systems (AVoCS) (2011)"},{"key":"9619_CR125","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: A verification infrastructure for permission-based reasoning. In: Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 41\u201362 (2016)","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"9619_CR126","doi-asserted-by":"crossref","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27 (1980)","DOI":"10.1145\/322186.322198"},{"key":"9619_CR127","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.entcs.2016.01.004","volume":"320","author":"O Nguena-Timo","year":"2016","unstructured":"Nguena-Timo, O., Langelier, G.: Test data generation for cyclic executives with CBMC and Frama-C: a case study. Electron. Notes Comput. Sci. 320, 35\u201351 (2016)","journal-title":"Electron. Notes Comput. Sci."},{"issue":"4","key":"9619_CR128","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1016\/j.ic.2006.08.009","volume":"205","author":"R Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557\u2013580 (2007)","journal-title":"Inf. Comput."},{"key":"9619_CR129","doi-asserted-by":"crossref","unstructured":"Odersky, M.: How to make destructive updates less destructive. In: Proceedings of the ACM Symposium on the Principles Of Programming Languages (POPL), pp. 25\u201336 (1991)","DOI":"10.1145\/99583.99590"},{"key":"9619_CR130","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Proceedings of the Workshop on Computer Science Logic (CSL), pp. 1\u201319. Springer-Verlag (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1","DOI":"10.1007\/3-540-44802-0_1"},{"key":"9619_CR131","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. In: Proceedings of the European Symposium on Programming (ESOP), pp. 439\u2013458 (2011)","DOI":"10.1007\/978-3-642-19718-5_23"},{"key":"9619_CR132","doi-asserted-by":"crossref","unstructured":"Pearce, D.J.: A calculus for constraint-based flow typing. In: Proceedings of the Workshop on Formal Techniques for Java-like Programs (FTFJP), p. Article 7 (2013)","DOI":"10.1145\/2489804.2489810"},{"key":"9619_CR133","doi-asserted-by":"crossref","unstructured":"Pearce, D.J.: Sound and complete flow typing with unions, intersections and negations. In: Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 335\u2013354 (2013)","DOI":"10.1007\/978-3-642-35873-9_21"},{"key":"9619_CR134","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":"9619_CR135","doi-asserted-by":"publisher","unstructured":"Pearce, D.J.: Array programming in Whiley. In: Proceedings of the Workshop on Libraries, Languages and Compilers for Array Programming (ARRAY) (2017). https:\/\/doi.org\/10.1145\/3091966.3091972","DOI":"10.1145\/3091966.3091972"},{"key":"9619_CR136","doi-asserted-by":"crossref","unstructured":"Pearce, D.J.: A lightweight formalism for reference lifetimes and borrowing in Rust. ACM Trans. Program. Lang. Syst. 43(1), Article 3 (2021)","DOI":"10.1145\/3443420"},{"key":"9619_CR137","doi-asserted-by":"crossref","unstructured":"Pearce, D.J., Groves, L.: Reflections on verifying software with Whiley. In: Proceedings of the Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), pp. 142\u2013159 (2013)","DOI":"10.1007\/978-3-319-05416-2_10"},{"key":"9619_CR138","doi-asserted-by":"crossref","unstructured":"Pearce, D.J., Groves, L.: Whiley: a platform for research in software verification. In: Proceedings of the Conference on Software Language Engineering (SLE), pp. 238\u2013248 (2013)","DOI":"10.1007\/978-3-319-02654-1_13"},{"key":"9619_CR139","doi-asserted-by":"crossref","unstructured":"Pearce, D.J., Groves, L.: Designing a verifying compiler: Lessons learned from developing Whiley. Science of Computer Programming, pp. 191\u2013220 (2015)","DOI":"10.1016\/j.scico.2015.09.006"},{"key":"9619_CR140","doi-asserted-by":"publisher","unstructured":"Pearce, D.J., Utting, M., Groves, L.: An introduction to software verification with Whiley. In: Engineering Trustworthy Software Systems (SETTS), pp. 1\u201337. Springer-Verlag (2019). https:\/\/doi.org\/10.1007\/978-3-030-17601-3_1","DOI":"10.1007\/978-3-030-17601-3_1"},{"key":"9619_CR141","doi-asserted-by":"crossref","unstructured":"Polikarpova, N., Furia, C.A., West, S.: To run what no one has run before: Executing an intermediate verification language. In: Proceedings of the Conference on Runtime Verification (RV), pp. 251\u2013268 (2013)","DOI":"10.1007\/978-3-642-40787-1_15"},{"key":"9619_CR142","doi-asserted-by":"crossref","unstructured":"Prevosto, V., Burghardt, J., Gerlach, J., Hartig, K., Pohl, H.W., V\u00f6llinger, K.: Formal specification and automated verification of railway software with Frama-C. In: International Conference on Industrial Informatics (INDIN), pp. 710\u2013715. IEEE (2013)","DOI":"10.1109\/INDIN.2013.6622971"},{"issue":"4","key":"9619_CR143","first-page":"543","volume":"16","author":"A Puccetti","year":"2010","unstructured":"Puccetti, A.: Static analysis of the XEN kernel using Frama-C. J. Univ. Comput. Sci. 16(4), 543\u2013553 (2010)","journal-title":"J. Univ. Comput. Sci."},{"key":"9619_CR144","doi-asserted-by":"crossref","unstructured":"Pugh, W.: The Omega test: A fast and practical integer programming algorithm for dependence analysis. In: Proceedings of the Conference on Supercomputing, pp. 4\u201313. IEEE Computer Society Press (1991)","DOI":"10.1145\/125826.125848"},{"key":"9619_CR145","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.W.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Proceedings of Conference on Computer Aided Verification (CAV), LNCS, vol. 9207, pp. 198\u2013216. Springer-Verlag (2015)","DOI":"10.1007\/978-3-319-21668-3_12"},{"key":"9619_CR146","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krstic, S., Deters, M., Barrett, C.W.: Quantifier instantiation techniques for finite model finding in SMT. In: Proceedings of the Conference on Automated Deduction (CADE), LNCS, vol. 7898, pp. 377\u2013391. Springer-Verlag (2013)","DOI":"10.1007\/978-3-642-38574-2_26"},{"key":"9619_CR147","doi-asserted-by":"crossref","unstructured":"Rinard, M.C.: Integrated reasoning and proof choice point selection in the Jahob system - mechanisms for program survival. In: Proceedings of the Conference on Automated Deduction (CADE), LNCS, vol. 5663, pp. 1\u201316. Springer-Verlag (2009)","DOI":"10.1007\/978-3-642-02959-2_1"},{"issue":"1","key":"9619_CR148","doi-asserted-by":"publisher","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. Log. Comput. 3(1), 47\u201361 (1993). https:\/\/doi.org\/10.1093\/logcom\/3.1.47","journal-title":"J. Log. Comput."},{"key":"9619_CR149","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":"9619_CR150","doi-asserted-by":"crossref","unstructured":"Segal, L., Chalin, P.: A comparison of intermediate verification languages: Boogie and Sireum\/Pilar. In: Proceedings of the Conference on Verified Software: Theories, Tools, Experiments (VSTTE), pp. 130\u2013145 (2012)","DOI":"10.1007\/978-3-642-27705-4_11"},{"key":"9619_CR151","doi-asserted-by":"crossref","unstructured":"Shankar, N.: Static analysis for safe destructive updates in a functional language. In: Proceedings of the Symposium Logic-Based Program Synthesis and Transformation (LOPSTR), pp. 1\u201324 (2001)","DOI":"10.1007\/3-540-45607-4_1"},{"key":"9619_CR152","doi-asserted-by":"crossref","unstructured":"Smans, J., Jacobs, B., Piessens, F.: VeriCool: An automatic verifier for a concurrent object-oriented language. In: Formal Methods for Open Object-Based Distributed Systems (FMOODS), pp. 220\u2013239 (2008)","DOI":"10.1007\/978-3-540-68863-1_14"},{"issue":"1","key":"9619_CR153","doi-asserted-by":"publisher","first-page":"2:1","DOI":"10.1145\/2160910.2160911","volume":"34","author":"J Smans","year":"2012","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34(1), 2:1-2:58 (2012). https:\/\/doi.org\/10.1145\/2160910.2160911","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9619_CR154","doi-asserted-by":"crossref","unstructured":"Smans, J., Jacobs, B., Piessens, F., Schulte, W.: An automatic verifier for Java-like programs based on dynamic frames. In: Proceedings of the Conference on Fundamental Approaches to Software Engineering, LNCS, vol. 4961, pp. 261\u2013275. Springer-Verlag (2008)","DOI":"10.1007\/978-3-540-78743-3_19"},{"key":"9619_CR155","doi-asserted-by":"crossref","unstructured":"Souyris, J., Wiels, V., Delmas, D., Delseny, H.: Formal verification of avionics software products. In: Proceedings of the Symposium on Formal Methods (FM), LNCS, vol. 5850, pp. 532\u2013546. Springer-Verlag (2009)","DOI":"10.1007\/978-3-642-05089-3_34"},{"key":"9619_CR156","unstructured":"Stevens, M.: Demonstrating Whiley on an embedded system. Tech. rep., School of Engineering and Computer Science, Victoria University of Wellington (2014). http:\/\/www.ecs.vuw.ac.nz\/~djp\/files\/MattStevensENGR489.pdf"},{"key":"9619_CR157","doi-asserted-by":"crossref","unstructured":"Ter-Gabrielyan, A., Summers, A.J., M\u00fcller, P.: Modular verification of heap reachability properties in separation logic. In: Proceedings of the ACM conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), p. Article 121. ACM Press (2019)","DOI":"10.1145\/3360547"},{"key":"9619_CR158","unstructured":"The Alt-Ergo automated theorem prover, http:\/\/alt-ergo.lri.fr\/"},{"key":"9619_CR159","unstructured":"The Whiley Programming Language. http:\/\/whiley.org"},{"key":"9619_CR160","doi-asserted-by":"crossref","unstructured":"Tobin-Hochstadt, S., Felleisen, M.: Logical types for untyped languages. In: Proceedings of the ACM International Conference on Functional Programming (ICFP), pp. 117\u2013128 (2010)","DOI":"10.1145\/1932681.1863561"},{"key":"9619_CR161","doi-asserted-by":"crossref","unstructured":"Toman, J., Pernsteiner, S., Torlak, E.: Crust: A bounded verifier for rust. In: Proceedings of the Conference on Automated Software Engineering (ASE), pp. 75\u201380 (2015)","DOI":"10.1109\/ASE.2015.77"},{"key":"9619_CR162","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Meyer, B.: Automatic verification of advanced object-oriented features: The AutoProof approach. In: LASER Summer School, LNCS, vol. 7682, pp. 133\u2013155. Springer (2011)","DOI":"10.1007\/978-3-642-35746-6_5"},{"key":"9619_CR163","doi-asserted-by":"crossref","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: Auto-active functional verification of object-oriented programs. In: Proceedings of the conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 9035, pp. 566\u2013580. Springer-Verlag (2015)","DOI":"10.1007\/978-3-662-46681-0_53"},{"key":"9619_CR164","doi-asserted-by":"crossref","unstructured":"Utting, M., Pearce, D.J., Groves, L.: Making Whiley Boogie! In: Proceedings of the Conference on Integrated Formal Methods (iFM), pp. 69\u201384 (2017)","DOI":"10.1007\/978-3-319-66845-1_5"},{"key":"9619_CR165","doi-asserted-by":"crossref","unstructured":"Volkov, G., Mandrykin, M.U., Efremov, D.: Lemma functions for Frama-C: C programs as proofs. CoRR arXiv:1811.05879 (2018)","DOI":"10.1109\/ISPRAS.2018.00012"},{"key":"9619_CR166","doi-asserted-by":"crossref","unstructured":"Wang, F., Song, F., Zhang, M., Zhu, X., Zhang, J.: Krust: A formal executable semantics of rust. In: Proceedings of the Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 44\u201351 (2018)","DOI":"10.1109\/TASE.2018.00014"},{"key":"9619_CR167","unstructured":"Weiss, A., Patterson, D., Matsakis, N.D., Ahmed, A.: Oxide: The essence of rust (2019)"},{"key":"9619_CR168","doi-asserted-by":"crossref","unstructured":"Weng, M., Utting, M., Pfahringer, B.: Bound analysis for Whiley programs. In: Proc. Usages of Symbolic Execution Workshop (2015)","DOI":"10.1016\/j.entcs.2016.01.005"},{"key":"9619_CR169","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.entcs.2016.01.005","volume":"320","author":"MH Weng","year":"2016","unstructured":"Weng, M.H., Utting, M., Pfahringer, B.: Bound analysis for Whiley programs. Electron. Notes Comput. Sci. 320, 53\u201367 (2016). https:\/\/doi.org\/10.1016\/j.entcs.2016.01.005","journal-title":"Electron. Notes Comput. Sci."},{"key":"9619_CR170","doi-asserted-by":"crossref","unstructured":"Xu, G.H., Yang, Z.: JMLAutoTest: A novel automated testing framework based on JML and JUnit. In: Proceedings of the Workshop on Formal Approaches to Testing of Software (FATES), pp. 70\u201385 (2003)","DOI":"10.1007\/978-3-540-24617-6_6"},{"key":"9619_CR171","doi-asserted-by":"publisher","unstructured":"Zimmerman, D.M., Nagmoti, R.: JMLUnit: The Next Generation. In: Proceedings of the Conference on Formal Verification of Object-Oriented Software, pp. 183\u2013197. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-18070-5_13","DOI":"10.1007\/978-3-642-18070-5_13"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09619-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09619-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09619-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,20]],"date-time":"2024-09-20T17:00:55Z","timestamp":1726851655000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09619-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,20]]},"references-count":171,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,11]]}},"alternative-id":["9619"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09619-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2022,3,20]]},"assertion":[{"value":"22 April 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 January 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 March 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}