Verifying Whiley programs with Boogie. (English) Zbl 1512.68059
Summary: 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 “high-level” 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’s 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.
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
Keywords:
Whiley; Boogie; verifying compiler; intermediate verification language; semantic translation; impedance mismatch; flow typing; verification conditionsSoftware:
JML; VAMPIRE; OpenJML; Joogie; KRAKATOA; GPUVerify; Toolchain; Rust; Crust; VeriCool; BVD; KLEE; ESC/Java; Frama-C; Alt-Ergo; Dafny; JUnit; AutoProof; VeriFast; Nagini; SMACK; Whiley; z3; KeY; Korat; CBMC; RustHorn; CVC4; Viper; Boogie; SMT-LIB; ACSL; WhyML; Scala; JMLUnit; AstraVer; VCC; Chalice; Jahob; RustBelt; JMLAutoTest; Whiteoak; Yices; VerCors; SIMPLIFY; Coq; Why3; Caduceus; Spec#; cvc3; EiffelReferences:
| [1] | 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-4:5. ACM Press (2015) |
| [2] | Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification—The KeY Book—From Theory to Practice, LNCS, vol. 10001. Springer (2016). doi:10.1007/978-3-319-49812-6 |
| [3] | 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-613. ACM Press (2011) |
| [4] | 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-95 (2016) |
| [5] | 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-216. Springer-Verlag (2014) · Zbl 1445.68131 |
| [6] | Appel, AW, Program Logics—for Certified Compilers (2014), Cambridge: Cambridge University Press, Cambridge · Zbl 1298.68009 · doi:10.1017/CBO9781107256552 |
| [7] | Arlt, S., Rümmer, P., Schäf, M.: Joogie: from Java through Jimple to Boogie. In: Proceedings of the Workshop on State of the Art in Java Program analysis (2013) |
| [8] | Astrauskas, V., Müller, 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) |
| [9] | 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-411. Springer-Verlag (2008). doi:10.1007/978-3-540-70592-5_17 |
| [10] | Bannwart, F.; Müller, P., A program logic for bytecode, Electron. Notes Comput. Sci., 141, 1, 255-273 (2005) · doi:10.1016/j.entcs.2005.02.026 |
| [11] | Baranowski, M., He, S., Rakamarić, Z.: Verifying Rust programs with SMACK. In: Automated Technology for Verification and Analysis, pp. 528-535. Springer-Verlag (2018) |
| [12] | Barbanera, F., Caglini, M.D.C.: Intersection and union types. In: Proceedings of the Conference on Theoretical Aspects of Computer Software (TACS), pp. 651-674 (1991) · Zbl 1493.68080 |
| [13] | Barnes, J.: High Integrity Ada: The SPARK Approach. Addison Wesley Longman, Inc., Reading (1997) · Zbl 0884.68017 |
| [14] | 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-387 (2006) |
| [15] | Barnett, M.; DeLine, R.; Fähndrich, M.; Leino, KRM; Schulte, W., Verification of object-oriented programs with invariants, J. Object Technol., 3, 6, 27-56 (2004) · doi:10.5381/jot.2004.3.6.a2 |
| [16] | Barnett, M.; Fähndrich, M.; Leino, KRM; Müller, P.; Schulte, W.; Venter, H., Specification and verification: the Spec# experience, Commun. ACM, 54, 6, 81-91 (2011) · doi:10.1145/1953122.1953145 |
| [17] | 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-87. ACM Press (2005) |
| [18] | 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-168. Springer-Verlag (2010) |
| [19] | Barrett, C., Tinelli, C.: CVC3. In: Proceedings of Conference on Computer Aided Verification (CAV), pp. 298-302 (2007) |
| [20] | 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-177. Springer-Verlag (2011) · Zbl 0714.65036 |
| [21] | 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 ’10) (2010) |
| [22] | Baudin, P., Cuo, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C specification language (version 1.8) |
| [23] | Beame, P.; Liew, V., Toward verifying nonlinear integer arithmetic, J. ACM, 66, 3, 22:1-22:30 (2019) · Zbl 1473.68105 · doi:10.1145/3319396 |
| [24] | Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer-Verlag (2004) · Zbl 1069.68095 |
| [25] | 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-132. ACM Press (2012) |
| [26] | 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-30. IEEE (2018) |
| [27] | 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-131. Springer-Verlag (2014) |
| [28] | Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Workshop on Intermediate Verification Languages (2011) |
| [29] | 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-46. Springer-Verlag (2018) |
| [30] | Bornat, R.: Proving pointer programs in Hoare logic. In: Proceedings of the Conference on the Mathematics of Program Construction (MPC) (2000) · Zbl 0963.68036 |
| [31] | 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-88 (2007) · Zbl 1132.68348 |
| [32] | 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-133 (2002). doi:10.1145/566171.566191 |
| [33] | Brandon, C., Chapin, P.: A SPARK/Ada cubesat control program. In: Proceedings of the Conference on Reliable Software Technologies (RST), pp. 51-64 (2013) |
| [34] | Burdy, L.; Cheon, Y.; Cok, DR; Ernst, MD; Kiniry, J.; Leavens, GT; Leino, KRM; Poll, E., An overview of JML tools and applications, Electron. Notes Comput. Sci., 80, 75-91 (2003) · doi:10.1016/S1571-0661(04)80810-7 |
| [35] | 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-224 (2008) |
| [36] | 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-79. ACM Press (1988) |
| [37] | Cataño, N., Huisman, M.: Formal specification and static checking of Gemplus’ electronic purse using ESC/Java. In: Proceedings of the Symposium on Formal Methods Europe (FME), LNCS, vol. 2391, pp. 272-289. Springer-Verlag (2002) · Zbl 1064.68577 |
| [38] | 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-363 (2005) |
| [39] | 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-261. Springer-Verlag (2008) |
| [40] | 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-26 (2014) |
| [41] | 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-108. Springer (2018) |
| [42] | 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-255. Springer (2002). doi:10.1007/3-540-47993-7_10 · Zbl 1049.68762 |
| [43] | Chin, J., Pearce, D.J.: Finding bugs with specification-based testing is easy! The Art, Science, and Engineering of Programming 5, Article 13 (2021) |
| [44] | 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-398. Springer-Verlag (2018) · Zbl 1511.68244 |
| [45] | 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-42. Springer-Verlag (2009) |
| [46] | Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Proceedings of the NASA Formal Methods Symposium, LNCS, vol. 6617, pp. 472-479. Springer-Verlag (2011) |
| [47] | 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-92 (2014) |
| [48] | 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-128 (2005) |
| [49] | Conchon, S., Coquereau, A., Iguernlala, M., Mebsout, A.: Alt-ergo 2.2. In: Workshop on Satisfiability Modulo Theories (SMT). HAL CCSD (2018) |
| [50] | 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-114 (2004) · Zbl 1081.68673 |
| [51] | Corzilius, F., Loup, U., Junges, S., Ábrahám, 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-448. Springer-Verlag (2012) |
| [52] | 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-247. Springer-Verlag (2012) |
| [53] | de Moura, L., Bjørner, 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-340 (2008) |
| [54] | de Moura, L.M., Bjørner, N.: Efficient E-matching for SMT solvers. In: Proceedings of the Conference on Automated Deduction (CADE), pp. 183-198 (2007) · Zbl 1213.68578 |
| [55] | Detlefs, D.; Nelson, G.; Saxe, JB, Simplify: a theorem prover for program checking, J. ACM, 52, 3, 365-473 (2005) · Zbl 1323.68462 · doi:10.1145/1066100.1066102 |
| [56] | Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. SRC Research Report 159, Compaq Systems Research Center (1998) |
| [57] | Dijkstra, EW, Guarded commands, nondeterminancy and formal derivation of programs, Commun. ACM, 18, 453-457 (1975) · Zbl 0308.68017 · doi:10.1145/360933.360975 |
| [58] | Dross, C., Efstathopoulos, P., Lesens, D., Mentré, D., Moy, Y.: Rail, space, security: three case studies for spark 2014. In: Proceedings of the Congress on Embedded Real Time Systems (ERTS) (2014) |
| [59] | Dross, C., Furia, C.A., Huisman, M., Monahan, R., Müller, P.: VerifyThis 2019: A program verification competition (extended report). CoRR arXiv:2008.13610 (2020) |
| [60] | Dubochet, G., Odersky, M.: Compiling structural types on the JVM: a comparison of reflective and generative techniques from scala’s perspective. In: Proceedings of the Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems Workshop (ICOOOLPS), pp. 34-41. ACM Press (2009) |
| [61] | Dutertre, B.: Yices 2.2. In: Proceedings of Conference on Computer Aided Verification (CAV), LNCS, vol. 8559, pp. 737-744. Springer-Verlag (2014) |
| [62] | Dutertre, B., de Moura, L.M.: A fast linear-arithmetic solver for DPLL(T). In: Proceedings of Conference on Computer Aided Verification (CAV), pp. 81-94 (2006) |
| [63] | Eilers, M., Müller, P.: Nagini: A static verifier for Python. In: Proceedings of Conference on Computer Aided Verification (CAV), LNCS, vol. 10981, pp. 596-603. Springer-Verlag (2018) |
| [64] | Fähndrich, 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-312. ACM Press (2003) |
| [65] | Filliâtre, J., Paskevich, A.: Why3—where programs meet provers. In: Proceedings of the European Symposium on Programming (ESOP), pp. 125-128 (2013) · Zbl 1435.68366 |
| [66] | Filliâtre, 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-97. Springer-Verlag (2012) |
| [67] | Filliâtre, J.C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Proceedings of Conference on Computer Aided Verification (CAV), LNCS, vol. 4590, pp. 173-177. Springer-Verlag (2007) |
| [68] | 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-245 (2002) |
| [69] | 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) |
| [70] | Games, M.: The fantastic combinations of John Conway’s new solitaire game “life” by Martin Gardner. Scientific American 223, 120-123 (1970) |
| [71] | Ge, Y., de Moura, L.M.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Proceedings of Conference on Computer Aided Verification (CAV), pp. 306-320 (2009) · Zbl 1242.68280 |
| [72] | 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-90. ACM Press (2008) |
| [73] | Goodloe, A.E., Muñoz, 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-446. Springer-Verlag (2013) |
| [74] | 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-414. Springer-Verlag (2011) |
| [75] | Gries, D.: The multiple assignment statement. IEEE Trans. Softw. Eng. 4, 89-93 (1978) · Zbl 0381.68017 |
| [76] | Gries, D., The Science of Programming (1981), Berlin: Springer-Verlag, Berlin · Zbl 0472.68003 · doi:10.1007/978-1-4612-5983-1 |
| [77] | 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-275 (2011) · Zbl 1326.68048 |
| [78] | 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-293 (2006) · Zbl 1178.68153 |
| [79] | Heule, S., Kassios, I.T., Müller, 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-476 (2013) |
| [80] | Hoare, C., The verifying compiler: a grand challenge for computing research, J. ACM, 50, 1, 63-69 (2003) · Zbl 1032.68868 · doi:10.1145/602382.602403 |
| [81] | 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-231. IEEE Computer Society (2014) |
| [82] | Hoder, K., Kovács, 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-64. Springer-Verlag (2011) |
| [83] | Huisman, M., Klebanov, V., Monahan, R.: VerifyThis verification competition 2016—organizer’s report (2013) |
| [84] | Igarashi, A., Nagira, H.: Union types for object-oriented programming. J. Obj. Technol. 6(2) (2007) |
| [85] | 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-55 (2011) |
| [86] | 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-311 (2010) |
| [87] | Jennings, TJ; Carré, BA, A subset of Ada for formal verification (SPARK), Ada User, 9, Supplement, 121-126 (1989) |
| [88] | 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-346. Springer-Verlag (2017) · Zbl 1484.68220 |
| [89] | 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) |
| [90] | 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-66:34. ACM Press (2018) |
| [91] | 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-283. Springer-Verlag (2006) |
| [92] | Kassios, I.T.: Dynamic frames and automated verification. Tech. Rep. Tutorial for the. 2nd COST Action IC0701 Training School (2011) · Zbl 1252.68192 |
| [93] | Klebanov, V., Müller, P., Shankar, N., Leavens, G.T., Wüstholz, 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ß, B.: The 1st verified software competition: Experience report (VSComp). In: Proceedings of the Symposium on Formal Methods (FM), LNCS. Springer-Verlag (2011) |
| [94] | 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-399. Springer-Verlag (2013) |
| [95] | Kovács, L., Voronkov, A.: First-order theorem proving and Vampire. In: Proceedings of Conference on Computer Aided Verification (CAV), LNCS, vol. 8044, pp. 1-35. Springer-Verlag (2013) |
| [96] | Kremer, G., Corzilius, F., Ábrahám, 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-335. Springer-Verlag (2016) · Zbl 1453.90186 |
| [97] | 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-391. Springer-Verlag (2014) |
| [98] | 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-41 (2011) |
| [99] | Leavens, GT; Cheon, Y.; Clifton, C.; Ruby, C.; Cok, DR, How the design of JML accommodates both runtime assertion checking and formal verification, Sci. Comput. Program., 55, 1-3, 185-208 (2005) · Zbl 1075.68009 · doi:10.1016/j.scico.2004.05.015 |
| [100] | 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) |
| [101] | Leino, KRM, Efficient weakest preconditions, Inf. Process. Lett., 93, 6, 281-288 (2005) · Zbl 1173.68563 · doi:10.1016/j.ipl.2004.10.015 |
| [102] | Leino, K.R.M.: Specification and verification of object-oriented software. Technical Report, Marktoberdorf Internation Summer School (2008) |
| [103] | 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 |
| [104] | 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-370. Springer-Verlag (2010) · Zbl 1253.68095 |
| [105] | 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) · Zbl 1326.68262 |
| [106] | 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-26 (2012) |
| [107] | 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-622 (2009) |
| [108] | 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-126. Springer-Verlag (2010) |
| [109] | Leino, K.R.M., Müller, P.: Using the Spec# language, methodology, and tools to write bug-free programs. In: LASER Summer School, LNCS, vol. 6029, pp. 91-139. Springer-Verlag (2008) |
| [110] | Leino, K.R.M., Müller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Foundations of Security Analysis and Design V (FOSAD), pp. 195-222 (2009) |
| [111] | 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-381. Springer-Verlag (2016) |
| [112] | Leino, K.R.M., Rümmer, 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-327. Springer-Verlag (2010) · Zbl 1284.68409 |
| [113] | 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) · Zbl 1153.68016 |
| [114] | Leino, K.R.M., Yessenov, K.: Stepwise refinement of heap-manipulating code in chalice. Formal Aspects of Computing 24(4-6) (2012) · Zbl 1259.68034 |
| [115] | Lindner, M., Aparicius, J., Lindgren, P.: No panic! verification of Rust programs by symbolic execution. In: International Conference on Industrial Informatics (INDIN), pp. 108-114 (2018) |
| [116] | 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. 1, pp. 432-439 (2019) |
| [117] | Malayeri, D., Aldrich, J.: Integrating nominal and structural subtyping. In: Proceedings of the European Conference on Object-Oriented Programming (ECOOP), pp. 260-284 (2008) |
| [118] | 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-111. Springer-Verlag (2009) |
| [119] | 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-120. Springer-Verlag (2016) |
| [120] | Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for Rust programs. In: Programming Languages and Systems, pp. 484-514. Springer-Verlag (2020) · Zbl 1508.68071 |
| [121] | McCormick, J.W., Chapin, P.C.: Building High Integrity Applications with SPARK. Cambridge University Press (2015). doi:10.1017/CBO9781139629294 · Zbl 1328.68009 |
| [122] | Meyer, B., Eiffel: a language and environment for software engineering, J. Syst. Softw., 8, 3, 199-246 (1988) · doi:10.1016/0164-1212(88)90022-2 |
| [123] | Meyer, B.: Applying “design by contract”. IEEE. Comput. 25(10), 40-51 (1992) |
| [124] | Mühlberg1and, J.T., Freitas, L.: Verifying freertos: from requirements to binary code. In: Proceedings of the Workshop on Automated Verification of Critical Systems (AVoCS) (2011) |
| [125] | Müller, 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-62 (2016) · Zbl 1475.68191 |
| [126] | Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27 (1980) · Zbl 0441.68111 |
| [127] | 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-51 (2016) · doi:10.1016/j.entcs.2016.01.004 |
| [128] | Nieuwenhuis, R.; Oliveras, A., Fast congruence closure and extensions, Inf. Comput., 205, 4, 557-580 (2007) · Zbl 1112.68116 · doi:10.1016/j.ic.2006.08.009 |
| [129] | Odersky, M.: How to make destructive updates less destructive. In: Proceedings of the ACM Symposium on the Principles Of Programming Languages (POPL), pp. 25-36 (1991) |
| [130] | O’Hearn, 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-19. Springer-Verlag (2001). doi:10.1007/3-540-44802-0_1 · Zbl 0999.68045 |
| [131] | 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-458 (2011) · Zbl 1326.68104 |
| [132] | 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) |
| [133] | 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-354 (2013) · Zbl 1427.68049 |
| [134] | 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-33 (2015) |
| [135] | Pearce, D.J.: Array programming in Whiley. In: Proceedings of the Workshop on Libraries, Languages and Compilers for Array Programming (ARRAY) (2017). doi:10.1145/3091966.3091972 |
| [136] | Pearce, D.J.: A lightweight formalism for reference lifetimes and borrowing in Rust. ACM Trans. Program. Lang. Syst. 43(1), Article 3 (2021) |
| [137] | 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-159 (2013) |
| [138] | 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-248 (2013) |
| [139] | Pearce, D.J., Groves, L.: Designing a verifying compiler: Lessons learned from developing Whiley. Science of Computer Programming, pp. 191-220 (2015) |
| [140] | Pearce, D.J., Utting, M., Groves, L.: An introduction to software verification with Whiley. In: Engineering Trustworthy Software Systems (SETTS), pp. 1-37. Springer-Verlag (2019). doi:10.1007/978-3-030-17601-3_1 |
| [141] | 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-268 (2013) |
| [142] | Prevosto, V., Burghardt, J., Gerlach, J., Hartig, K., Pohl, H.W., Völlinger, K.: Formal specification and automated verification of railway software with Frama-C. In: International Conference on Industrial Informatics (INDIN), pp. 710-715. IEEE (2013) |
| [143] | Puccetti, A., Static analysis of the XEN kernel using Frama-C, J. Univ. Comput. Sci., 16, 4, 543-553 (2010) |
| [144] | Pugh, W.: The Omega test: A fast and practical integer programming algorithm for dependence analysis. In: Proceedings of the Conference on Supercomputing, pp. 4-13. IEEE Computer Society Press (1991) |
| [145] | 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-216. Springer-Verlag (2015) · Zbl 1381.68059 |
| [146] | 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-391. Springer-Verlag (2013) · Zbl 1381.68275 |
| [147] | 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-16. Springer-Verlag (2009) |
| [148] | Robison, PJ; Staples, J., Formalizing a hierarchical structure of practical mathematical reasoning, J. Log. Comput., 3, 1, 47-61 (1993) · Zbl 0779.68078 · doi:10.1093/logcom/3.1.47 |
| [149] | Sánchez, 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-18. ACM Press (2014) |
| [150] | 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-145 (2012) |
| [151] | 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-24 (2001) · Zbl 1073.68564 |
| [152] | 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-239 (2008) |
| [153] | Smans, J.; Jacobs, B.; Piessens, F., Implicit dynamic frames, ACM Trans. Program. Lang. Syst., 34, 1, 2:1-2:58 (2012) · doi:10.1145/2160910.2160911 |
| [154] | 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-275. Springer-Verlag (2008) |
| [155] | 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-546. Springer-Verlag (2009) |
| [156] | 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 |
| [157] | Ter-Gabrielyan, A., Summers, A.J., Müller, 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) |
| [158] | The Alt-Ergo automated theorem prover, http://alt-ergo.lri.fr/ |
| [159] | The Whiley Programming Language. http://whiley.org |
| [160] | Tobin-Hochstadt, S., Felleisen, M.: Logical types for untyped languages. In: Proceedings of the ACM International Conference on Functional Programming (ICFP), pp. 117-128 (2010) · Zbl 1323.68083 |
| [161] | Toman, J., Pernsteiner, S., Torlak, E.: Crust: A bounded verifier for rust. In: Proceedings of the Conference on Automated Software Engineering (ASE), pp. 75-80 (2015) |
| [162] | 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-155. Springer (2011) |
| [163] | 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-580. Springer-Verlag (2015) |
| [164] | Utting, M., Pearce, D.J., Groves, L.: Making Whiley Boogie! In: Proceedings of the Conference on Integrated Formal Methods (iFM), pp. 69-84 (2017) · Zbl 1512.68059 |
| [165] | Volkov, G., Mandrykin, M.U., Efremov, D.: Lemma functions for Frama-C: C programs as proofs. CoRR arXiv:1811.05879 (2018) |
| [166] | 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-51 (2018) |
| [167] | Weiss, A., Patterson, D., Matsakis, N.D., Ahmed, A.: Oxide: The essence of rust (2019) |
| [168] | Weng, M., Utting, M., Pfahringer, B.: Bound analysis for Whiley programs. In: Proc. Usages of Symbolic Execution Workshop (2015) |
| [169] | Weng, MH; Utting, M.; Pfahringer, B., Bound analysis for Whiley programs, Electron. Notes Comput. Sci., 320, 53-67 (2016) · doi:10.1016/j.entcs.2016.01.005 |
| [170] | 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-85 (2003) |
| [171] | Zimmerman, D.M., Nagmoti, R.: JMLUnit: The Next Generation. In: Proceedings of the Conference on Formal Verification of Object-Oriented Software, pp. 183-197. Springer (2010). doi:10.1007/978-3-642-18070-5_13 · Zbl 1308.68032 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
