{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,8]],"date-time":"2024-07-08T10:49:51Z","timestamp":1720435791915},"reference-count":129,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2015,12,1]],"date-time":"2015-12-01T00:00:00Z","timestamp":1448928000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2019,12,1]],"date-time":"2019-12-01T00:00:00Z","timestamp":1575158400000},"content-version":"vor","delay-in-days":1461,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"funder":[{"DOI":"10.13039\/501100001509","name":"Royal Society of New Zealand","doi-asserted-by":"publisher","award":["VUW1105"],"id":[{"id":"10.13039\/501100001509","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2015,12]]},"DOI":"10.1016\/j.scico.2015.09.006","type":"journal-article","created":{"date-parts":[[2015,10,24]],"date-time":"2015-10-24T22:09:36Z","timestamp":1445724576000},"page":"191-220","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":14,"special_numbering":"P2","title":["Designing a verifying compiler: Lessons learned from developing Whiley"],"prefix":"10.1016","volume":"113","author":[{"given":"David J.","family":"Pearce","sequence":"first","affiliation":[]},{"given":"Lindsay","family":"Groves","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"1","key":"10.1016\/j.scico.2015.09.006_br0010","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1145\/602382.602403","article-title":"The verifying compiler: a grand challenge for computing research","volume":"50","author":"Hoare","year":"2003","journal-title":"J. ACM"},{"key":"10.1016\/j.scico.2015.09.006_br0020","series-title":"A program verifier","author":"King","year":"1969"},{"key":"10.1016\/j.scico.2015.09.006_br0030","series-title":"An interactive program verifier","author":"Deutsch","year":"1973"},{"key":"10.1016\/j.scico.2015.09.006_br0040","series-title":"Mathematical Logic and Programming Languages","first-page":"55","article-title":"Mechanical proofs about computer programs","author":"Good","year":"1985"},{"key":"10.1016\/j.scico.2015.09.006_br0050","series-title":"Stanford Pascal verifier user manual","author":"Luckham","year":"1979"},{"key":"10.1016\/j.scico.2015.09.006_br0060","series-title":"Extended static checking","author":"Detlefs","year":"1998"},{"key":"10.1016\/j.scico.2015.09.006_br0070","series-title":"Proceedings of the ACM Conference on Programming Language Design and Implementation","first-page":"234","article-title":"Extended static checking for Java","author":"Flanagan","year":"2002"},{"issue":"1\u20133","key":"10.1016\/j.scico.2015.09.006_br0080","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/j.scico.2004.05.015","article-title":"How the design of JML accommodates both runtime assertion checking and formal verification","volume":"55","author":"Leavens","year":"2005","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.scico.2015.09.006_br0090","series-title":"Proceedings of the Conference on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","first-page":"108","article-title":"ESC\/Java2: uniting ESC\/Java and JML","volume":"vol. 3362","author":"Cok","year":"2005"},{"issue":"6","key":"10.1016\/j.scico.2015.09.006_br0100","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1145\/1953122.1953145","article-title":"Specification and verification: the Spec# experience","volume":"54","author":"Barnett","year":"2011","journal-title":"Commun. ACM"},{"issue":"6","key":"10.1016\/j.scico.2015.09.006_br0110","doi-asserted-by":"crossref","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","article-title":"Verification of object-oriented programs with invariants","volume":"3","author":"Barnett","year":"2004","journal-title":"J. Object Technol."},{"key":"10.1016\/j.scico.2015.09.006_br0120","series-title":"Proceedings of the Conference on Logic for Programming, Artificial Intelligence, and Reasoning","first-page":"348","article-title":"Dafny: an automatic program verifier for functional correctness","volume":"vol. 6355","author":"Leino","year":"2010"},{"key":"10.1016\/j.scico.2015.09.006_br0130","series-title":"Proceedings of the Conference on Verified Software: Theories, Tools, Experiments","first-page":"82","article-title":"Developing verified programs with Dafny","volume":"vol. 7152","author":"Leino","year":"2012"},{"key":"10.1016\/j.scico.2015.09.006_br0140","series-title":"Proceedings of the European Symposium on Programming","first-page":"125","article-title":"Why3 \u2014 where programs meet provers","author":"Filli\u00e2tre","year":"2013"},{"key":"10.1016\/j.scico.2015.09.006_br0150","series-title":"Proceedings of the Asian Symposium on Programming Languages and Systems","first-page":"304","article-title":"A quick tour of the VeriFast program verifier","author":"Jacobs","year":"2010"},{"key":"10.1016\/j.scico.2015.09.006_br0160","series-title":"Proceedings of the NASA Formal Methods Symposium","first-page":"41","article-title":"VeriFast: a powerful, sound, predictable, fast verifier for C and Java","author":"Jacobs","year":"2011"},{"issue":"3","key":"10.1016\/j.scico.2015.09.006_br0170","doi-asserted-by":"crossref","DOI":"10.1145\/1353445.1353446","article-title":"The pitfalls of verifying floating-point computations","volume":"30","author":"Monniaux","year":"2008","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.scico.2015.09.006_br0180","series-title":"Informatics \u2014 10 Years Back, 10 Years Ahead","first-page":"157","article-title":"Extended static checking: a ten-year perspective","volume":"vol. 2000","author":"Leino","year":"2001"},{"key":"10.1016\/j.scico.2015.09.006_br0190","series-title":"Proceedings of the Software Engineering Workshop","first-page":"204","article-title":"Abstracting pointers for a verifying compiler","author":"Kulczycki","year":"2007"},{"key":"10.1016\/j.scico.2015.09.006_br0200","series-title":"Proceedings of the European Conference on Object-Oriented Programming","first-page":"491","article-title":"Object invariants in dynamic contexts","author":"Leino","year":"2004"},{"key":"10.1016\/j.scico.2015.09.006_br0210","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1145\/1941487.1941509","article-title":"Proving program termination","author":"Cook","year":"2011","journal-title":"Commun. ACM"},{"key":"10.1016\/j.scico.2015.09.006_br0220","series-title":"Formal Methods for Open Object-Based Distributed Systems","first-page":"220","article-title":"VeriCool: an automatic verifier for a concurrent object-oriented language","author":"Smans","year":"2008"},{"key":"10.1016\/j.scico.2015.09.006_br0230","series-title":"Proceedings of the Conference on Theorem Proving in Higher Order Logics","first-page":"23","article-title":"VCC: a practical system for verifying concurrent C","author":"Cohen","year":"2009"},{"key":"10.1016\/j.scico.2015.09.006_br0250","series-title":"Proceedings of the Conference on Software Language Engineering","first-page":"238","article-title":"Whiley: a platform for research in software verification","author":"Pearce","year":"2013"},{"key":"10.1016\/j.scico.2015.09.006_br0260","series-title":"Proceedings of the Conference on Software Language Engineering","article-title":"The Whiley Rewrite Language (WyRL)","author":"Pearce","year":"2015"},{"issue":"1","key":"10.1016\/j.scico.2015.09.006_br0270","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/j.entcs.2011.11.005","article-title":"Implementing a language with flow-sensitive and structural typing on the JVM","volume":"279","author":"Pearce","year":"2011","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"10.1016\/j.scico.2015.09.006_br0280","series-title":"Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation","first-page":"335","article-title":"Sound and complete flow typing with unions, intersections and negations","author":"Pearce","year":"2013"},{"key":"10.1016\/j.scico.2015.09.006_br0290","series-title":"Proceedings of the IEEE\/IFIP Workshop on Software Technologies for Future Embedded and Ubiquitous Systems","first-page":"26","article-title":"Integer range analysis for Whiley on embedded systems","author":"Pearce","year":"2015"},{"key":"10.1016\/j.scico.2015.09.006_br0300","series-title":"Proceedings of the Australasian Software Engineering Conference","first-page":"181","article-title":"OwnKit: inferring modularly checkable ownership annotations for Java","author":"Dymnikov","year":"2013"},{"key":"10.1016\/j.scico.2015.09.006_br0310","series-title":"Proceedings of the Workshop on Formal Verification of Object-Oriented Software","first-page":"3","article-title":"The COST IC0701 verification competition 2011","volume":"vol. 7421","author":"Bormer","year":"2011"},{"key":"10.1016\/j.scico.2015.09.006_br0320","series-title":"Proceedings of the Symposium on Formal Methods","article-title":"The 1st verified software competition: experience report (VSComp)","author":"Klebanov","year":"2011"},{"key":"10.1016\/j.scico.2015.09.006_br0330","unstructured":"D.J. Pearce, The Whiley language specification, Updated, 2014."},{"key":"10.1016\/j.scico.2015.09.006_br0340","unstructured":"D.J. Pearce, Getting started with Whiley, Last updated, 2014."},{"key":"10.1016\/j.scico.2015.09.006_br0350","series-title":"Proceedings of the ACM International Conference on Functional Programming","first-page":"117","article-title":"Logical types for untyped languages","author":"Tobin-Hochstadt","year":"2010"},{"key":"10.1016\/j.scico.2015.09.006_br0360","series-title":"Proceedings of the European Symposium on Programming","first-page":"256","article-title":"Typing local control and state using flow analysis","author":"Guha","year":"2011"},{"key":"10.1016\/j.scico.2015.09.006_br0370","series-title":"Proceedings of the Workshop on Formal Techniques for Java-Like Programs","first-page":"7","article-title":"A calculus for constraint-based flow typing","author":"Pearce","year":"2013"},{"key":"10.1016\/j.scico.2015.09.006_br0380","series-title":"Proceedings of the Conference on Theoretical Aspects of Computer Software","first-page":"651","article-title":"Intersection and union types","author":"Barbanera","year":"1991"},{"issue":"2","key":"10.1016\/j.scico.2015.09.006_br0390","doi-asserted-by":"crossref","first-page":"47","DOI":"10.5381\/jot.2007.6.2.a3","article-title":"Union types for object-oriented programming","volume":"6","author":"Igarashi","year":"2007","journal-title":"J. Object Technol."},{"key":"10.1016\/j.scico.2015.09.006_br0400","series-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"10.1016\/j.scico.2015.09.006_br0410","series-title":"QCon","article-title":"Null references: the billion dollar mistake","author":"Hoare","year":"2009"},{"key":"10.1016\/j.scico.2015.09.006_br0420","series-title":"Proceedings of the ACM conference on Object-Oriented Programming, Systems, Languages and Applications","first-page":"302","article-title":"Declaring and checking non-null types in an object-oriented language","author":"F\u00e4hndrich","year":"2003"},{"issue":"9","key":"10.1016\/j.scico.2015.09.006_br0430","doi-asserted-by":"crossref","first-page":"455","DOI":"10.5381\/jot.2007.6.9.a23","article-title":"Pluggable checking and inferencing of non-null types for Java","volume":"6","author":"Ekman","year":"2007","journal-title":"J. Object Technol."},{"key":"10.1016\/j.scico.2015.09.006_br0440","series-title":"Proceedings of the European Conference on Object-Oriented Programming","first-page":"227","article-title":"Non-null references by default in Java: alleviating the nullity annotation burden","author":"Chalin","year":"2007"},{"key":"10.1016\/j.scico.2015.09.006_br0450","series-title":"Proceedings of the conference on Compiler Construction","first-page":"229","article-title":"Java bytecode verification for @NonNull types","author":"Male","year":"2008"},{"key":"10.1016\/j.scico.2015.09.006_br0460","series-title":"Proceedings of the Workshop on Program Analysis for Software Tools and Engineering","first-page":"36","article-title":"A non-null annotation inferencer for Java bytecode","author":"Hubert","year":"2008"},{"key":"10.1016\/j.scico.2015.09.006_br0470","series-title":"Proceedings of the Conference on Principles and Practices of Programming in Java","first-page":"135","article-title":"Propagation of JML non-null annotations in Java programs","author":"Cielecki","year":"2006"},{"key":"10.1016\/j.scico.2015.09.006_br0480","series-title":"Proceedings of the International Conference on Formal Methods for Open Object-Based Distributed Systems","first-page":"132","article-title":"Semantic foundations and inference of non-null annotations","author":"Hubert","year":"2008"},{"key":"10.1016\/j.scico.2015.09.006_br0490","unstructured":"ISO\/IEC, International standard ISO\/IEC 9899, programming languages \u2014 C, 1990."},{"key":"10.1016\/j.scico.2015.09.006_br0500","series-title":"Practical verification condition generation for a bytecode language","author":"Pearce","year":"2014"},{"key":"10.1016\/j.scico.2015.09.006_br0510","series-title":"Proceedings of the conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"337","article-title":"Z3: an efficient SMT solver","author":"de Moura","year":"2008"},{"issue":"3","key":"10.1016\/j.scico.2015.09.006_br0520","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","article-title":"Simplify: a theorem prover for program checking","volume":"52","author":"Detlefs","year":"2005","journal-title":"J. ACM"},{"key":"10.1016\/j.scico.2015.09.006_br0530","series-title":"Proceedings of the ACM symposium on the Principles Of Programming Languages","first-page":"25","article-title":"An efficient method of computing static single assignment form","author":"Cytron","year":"1989"},{"key":"10.1016\/j.scico.2015.09.006_br0540","first-page":"19","article-title":"Assigning meaning to programs","volume":"vol. 19","author":"Floyd","year":"1967"},{"key":"10.1016\/j.scico.2015.09.006_br0550","series-title":"Proceedings of the conference on Compiler Construction","first-page":"104","article-title":"JPure: a modular purity system for Java","author":"Pearce","year":"2011"},{"key":"10.1016\/j.scico.2015.09.006_br0560","series-title":"Proceedings of the International Conference on Software Maintenance","first-page":"82","article-title":"Precise identification of side-effect-free methods in Java","author":"Rountev","year":"2004"},{"key":"10.1016\/j.scico.2015.09.006_br0570","series-title":"Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation","first-page":"199","article-title":"Purity and side effect analysis for Java programs","author":"Salcianu","year":"2005"},{"key":"10.1016\/j.scico.2015.09.006_br0580","series-title":"Proceedings of the International Symposium on Software Testing and Analysis","first-page":"1","article-title":"Parameterized object sensitivity for points-to and side-effect analyses for Java","author":"Milanova","year":"2002"},{"key":"10.1016\/j.scico.2015.09.006_br0590","series-title":"Workshop on Specification and Verification of Component-Based Systems","first-page":"43","article-title":"Extensions of the theory of observational purity and a practical design for JML","author":"Cok","year":"2008"},{"key":"10.1016\/j.scico.2015.09.006_br0600","series-title":"Proceedings of the Symposium on Formal Methods","first-page":"268","article-title":"Dynamic frames: support for framing, dependencies and sharing without restrictions","volume":"vol. 4085","author":"Kassios","year":"2006"},{"key":"10.1016\/j.scico.2015.09.006_br0610","series-title":"Proceedings of the Conference on Compiler Construction","first-page":"22","article-title":"Staged static techniques to efficiently implement array copy semantics in a MATLAB JIT compiler","author":"Lameed","year":"2011"},{"key":"10.1016\/j.scico.2015.09.006_br0620","series-title":"Proceedings of the Symposium Logic-Based Program Synthesis and Transformation","first-page":"1","article-title":"Static analysis for safe destructive updates in a functional language","author":"Shankar","year":"2001"},{"key":"10.1016\/j.scico.2015.09.006_br0630","series-title":"Proceedings of the ACM symposium on the Principles Of Programming Languages","first-page":"25","article-title":"How to make destructive updates less destructive","author":"Odersky","year":"1991"},{"key":"10.1016\/j.scico.2015.09.006_br0640","series-title":"Proceedings of the conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"358","article-title":"Deciding bit-vector arithmetic with abstraction","author":"Bryant","year":"2007"},{"key":"10.1016\/j.scico.2015.09.006_br0650","series-title":"The VeriFast program verifier: a tutorial","author":"Jacobs","year":"2014"},{"key":"10.1016\/j.scico.2015.09.006_br0660","series-title":"Principles of Program Analysis","author":"Nielson","year":"1999"},{"key":"10.1016\/j.scico.2015.09.006_br0670","series-title":"Proceedings of the ACM symposium on the Principles Of Programming Languages","first-page":"235","article-title":"Sound compilation of reals","author":"Darulova","year":"2014"},{"key":"10.1016\/j.scico.2015.09.006_br0680","series-title":"Proceedings of the Symposium on Formal Methods","first-page":"246","article-title":"JML runtime assertion checking: improved error reporting and efficiency using strong validity","volume":"vol. 5014","author":"Chalin","year":"2008"},{"key":"10.1016\/j.scico.2015.09.006_br0690","series-title":"Proceedings of the ACM symposium on the Principles Of Programming Languages","first-page":"318","article-title":"Executable specifications with quantifiers in the FASE system","author":"Jefferson","year":"1986"},{"issue":"5","key":"10.1016\/j.scico.2015.09.006_br0700","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1049\/sej.1992.0033","article-title":"Specifications are (preferably) executable","volume":"7","author":"Fuchs","year":"1992","journal-title":"Softw. Eng. J."},{"issue":"10","key":"10.1016\/j.scico.2015.09.006_br0710","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An axiomatic basis for computer programming","volume":"12","author":"Hoare","year":"1969","journal-title":"Commun. ACM"},{"key":"10.1016\/j.scico.2015.09.006_br0720","series-title":"Proceedings of the Mexican International Conference on Artificial Intelligence","first-page":"190","article-title":"Invariant patterns for program reasoning","volume":"vol. 2972","author":"Ireland","year":"2004"},{"key":"10.1016\/j.scico.2015.09.006_br0730","series-title":"Proceedings of the Formal Methods for Components and Objects","first-page":"364","article-title":"Boogie: a modular reusable verifier for object-oriented programs","author":"Barnett","year":"2006"},{"key":"10.1016\/j.scico.2015.09.006_br0740","author":"Furia"},{"key":"10.1016\/j.scico.2015.09.006_br0750","series-title":"Proceedings of the International Symposium on Software Testing and Analysis","first-page":"93","article-title":"A comparative study of programmer-written and automatically inferred contracts","author":"Polikarpova","year":"2009"},{"key":"10.1016\/j.scico.2015.09.006_br0760","series-title":"Proceedings of the ACM Symposium on the Principles Of Programming Languages","first-page":"191","article-title":"Predicate abstraction for software verification","author":"Flanagan","year":"2002"},{"issue":"5 & 6","key":"10.1016\/j.scico.2015.09.006_br0770","doi-asserted-by":"crossref","first-page":"705","DOI":"10.1016\/S0747-7171(06)80010-6","article-title":"On the mechanical derivation of loop invariants","volume":"15","author":"Chadha","year":"1993","journal-title":"J. Symb. Comput."},{"key":"10.1016\/j.scico.2015.09.006_br0780","series-title":"Proceedings of the Asian Symposium on Programming Languages and Systems","first-page":"119","article-title":"Loop invariants on demand","volume":"vol. 3780","author":"Leino","year":"2005"},{"key":"10.1016\/j.scico.2015.09.006_br0790","series-title":"Proceedings of the Symposium on Formal Methods","first-page":"37","article-title":"Maximal and compositional pattern-based loop invariants","volume":"vol. 7436","author":"Aponte","year":"2012"},{"key":"10.1016\/j.scico.2015.09.006_br0800","series-title":"Proceedings of the Static Analysis Symposium","first-page":"58","article-title":"Inference of polynomial invariants for imperative programs: a farewell to Gr\u00f6bner bases","volume":"vol. 7460","author":"Cachera","year":"2012"},{"key":"10.1016\/j.scico.2015.09.006_br0810","unstructured":"F. Bobot, J.-C. Filli\u00e2tre, C. March\u00e9, G. Melquiond, A. Paskevich, The Why3 platform, v0.85, 2014."},{"key":"10.1016\/j.scico.2015.09.006_br0820","series-title":"Proceedings of the International Conference on Formal Engineering Methods","first-page":"315","article-title":"An improved rule for while loops in deductive program verification","author":"Beckert","year":"2005"},{"key":"10.1016\/j.scico.2015.09.006_br0830","series-title":"Proceedings of the Workshop on Program Analysis for Software Tools and Engineering","first-page":"82","article-title":"Weakest-precondition of unstructured programs","author":"Barnett","year":"2005"},{"key":"10.1016\/j.scico.2015.09.006_br0840","series-title":"Proceedings of the Conference on Theorem Proving in Higher Order Logics","first-page":"23","article-title":"VCC: a practical system for verifying concurrent C","volume":"vol. 5674","author":"Cohen","year":"2009"},{"key":"10.1016\/j.scico.2015.09.006_br0850","series-title":"Proceedings of the Conference on Software Engineering and Formal Methods","first-page":"317","article-title":"Adjusted verification rules for loops are more complete and give better diagnostics for less","author":"Chalin","year":"2009"},{"issue":"4","key":"10.1016\/j.scico.2015.09.006_br0860","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1007\/BF00289504","article-title":"An axiomatic definition of the programming language PASCAL","volume":"2","author":"Hoare","year":"1973","journal-title":"Acta Inform."},{"key":"10.1016\/j.scico.2015.09.006_br0870","series-title":"The Design of Well-Structured and Correct Programs","author":"Alagic","year":"1978"},{"key":"10.1016\/j.scico.2015.09.006_br0880","author":"Cohen"},{"key":"10.1016\/j.scico.2015.09.006_br0890","series-title":"LASER Summer School","first-page":"91","article-title":"Using the Spec# language, methodology, and tools to write bug-free programs","volume":"vol. 6029","author":"Leino","year":"2008"},{"key":"10.1016\/j.scico.2015.09.006_br0900","series-title":"Proceedings of the ACM Conference on Object-Oriented Programming, Systems, Languages and Applications","first-page":"113","article-title":"GPUVerify: a verifier for GPU kernels","author":"Betts","year":"2012"},{"key":"10.1016\/j.scico.2015.09.006_br0910","series-title":"Proceedings of the Conference on Software Engineering and Formal Methods","first-page":"233","article-title":"Frama-C: a software analysis perspective","volume":"vol. 7504","author":"Cuoq","year":"2012"},{"key":"10.1016\/j.scico.2015.09.006_br0920","series-title":"Proceedings of the European Symposium on Programming","first-page":"279","article-title":"Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions","volume":"vol. 3924","author":"Gulwani","year":"2006"},{"key":"10.1016\/j.scico.2015.09.006_br0930","series-title":"Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"407","article-title":"Zeno: an automated prover for properties of recursive data structures","volume":"vol. 7214","author":"Sonnex","year":"2012"},{"key":"10.1016\/j.scico.2015.09.006_br0940","series-title":"Proceedings of the European Conference on Object-Oriented Programming","first-page":"614","article-title":"Lightweight support for magic wands in an automatic verifier","volume":"vol. 37","author":"Schwerhoff","year":"2015"},{"key":"10.1016\/j.scico.2015.09.006_br0950","series-title":"Proceedings of the Conference on Automated Deduction","first-page":"167","article-title":"Solving quantified verification conditions using satisfiability modulo theories","volume":"vol. 4603","author":"Ge","year":"2007"},{"key":"10.1016\/j.scico.2015.09.006_br0960","series-title":"Proceedings of the Workshop on Formal Techniques for Java-like Programs","article-title":"Automatic verification of textbook programs that use comprehensions","author":"Leino","year":"2007"},{"key":"10.1016\/j.scico.2015.09.006_br0970","series-title":"Proceedings of the ACM Symposium on the Principles Of Programming Languages","first-page":"171","article-title":"Back to the future: revisiting precise program verification using SMT solvers","author":"Lahiri","year":"2008"},{"key":"10.1016\/j.scico.2015.09.006_br0980","series-title":"Proceedings of the Workshop on Constraints in Formal Verification","article-title":"Z310: applications, enablers, challenges and directions","author":"Bj\u00f8rner","year":"2009"},{"key":"10.1016\/j.scico.2015.09.006_br0990","series-title":"Proceedings of the International Workshop on Satisfiability Modulo Theories","first-page":"20","article-title":"Programming with triggers","author":"Moskal","year":"2009"},{"key":"10.1016\/j.scico.2015.09.006_br1000","article-title":"Programming: The Derivation of Algorithms","author":"Kaldewau","year":"1990"},{"key":"10.1016\/j.scico.2015.09.006_br1010","series-title":"Proceedings of the Conference on Formal Verification of Object-Oriented Software","first-page":"76","article-title":"Satisfiability solving and model generation for quantified first-order logic formulas","volume":"vol. 6528","author":"Gladisch","year":"2010"},{"key":"10.1016\/j.scico.2015.09.006_br1020","series-title":"Demonstrating Whiley on an embedded system","author":"Stevens","year":"2014"},{"key":"10.1016\/j.scico.2015.09.006_br1040","author":"Poss"},{"key":"10.1016\/j.scico.2015.09.006_br1050","series-title":"Verifying Whiley programs using an off-the-shelf SMT solver","author":"Wylde","year":"2014"},{"key":"10.1016\/j.scico.2015.09.006_br1060","series-title":"Proceedings of the Conference on Automated Deduction","article-title":"A proposal for a theory of finite sets, lists, and maps for the SMT-lib standard","author":"Kr\u00f6ning","year":"2009"},{"key":"10.1016\/j.scico.2015.09.006_br1070","series-title":"Proceedings of the Symposium on Formal Methods Europe","first-page":"272","article-title":"Formal specification and static checking of Gemplus' electronic purse using ESC\/Java","volume":"vol. 2391","author":"Cata\u00f1o","year":"2002"},{"key":"10.1016\/j.scico.2015.09.006_br1080","series-title":"Proceedings of the Workshop on Formal Integrated Development Environment","first-page":"79","article-title":"OpenJML: software verification for Java 7 using JML, OpenJDK, and eclipse","volume":"vol. 149","author":"Cok","year":"2014"},{"key":"10.1016\/j.scico.2015.09.006_br1090","series-title":"Proceedings of the Workshop on Foundations of Aspect-Oriented Languages","first-page":"13","article-title":"Static verification of PtolemyRely programs using OpenJML","author":"S\u00e1nchez","year":"2014"},{"key":"10.1016\/j.scico.2015.09.006_br1100","series-title":"Proceedings of the NASA Formal Methods Symposium","first-page":"472","article-title":"OpenJML: JML for Java 7 by extending OpenJDK","volume":"vol. 6617","author":"Cok","year":"2011"},{"key":"10.1016\/j.scico.2015.09.006_br1110","series-title":"Proceedings of the Conference on Verified Software: Theories, Tools, Experiments","first-page":"112","article-title":"Dafny meets the verification benchmarks challenge","volume":"vol. 6217","author":"Leino","year":"2010"},{"key":"10.1016\/j.scico.2015.09.006_br1120","series-title":"VerifyThis verification competition 2012","author":"Huisman","year":"2013"},{"key":"10.1016\/j.scico.2015.09.006_br1130","series-title":"Proceedings of the Workshop on Intermediate Verification Languages","article-title":"Why3: shepherd your herd of provers","author":"Bobot","year":"2011"},{"key":"10.1016\/j.scico.2015.09.006_br1140","series-title":"Proceedings of the Conference on Verified Software: Theories, Tools, Experiments","first-page":"83","article-title":"Verifying two lines of C with Why3: an exercise in program verification","volume":"vol. 7152","author":"Filli\u00e2tre","year":"2012"},{"key":"10.1016\/j.scico.2015.09.006_br1160","series-title":"Proceedings of Conference on Computer Aided Verification","first-page":"298","article-title":"CVC3","author":"Barrett","year":"2007"},{"key":"10.1016\/j.scico.2015.09.006_br1170","article-title":"Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions","author":"Bertot","year":"2004"},{"key":"10.1016\/j.scico.2015.09.006_br1180","series-title":"Proceedings of Conference on Computer Aided Verification","first-page":"173","article-title":"The Why\/Krakatoa\/Caduceus platform for deductive program verification","volume":"vol. 4590","author":"Filli\u00e2tre","year":"2007"},{"key":"10.1016\/j.scico.2015.09.006_br1190","series-title":"Proceedings of the NASA Formal Methods Symposium","first-page":"441","article-title":"Verification of numerical programs: from real numbers to floating point numbers","volume":"vol. 7871","author":"Goodloe","year":"2013"},{"key":"10.1016\/j.scico.2015.09.006_br1200","series-title":"Proceedings of the Symposium on Formal Methods","first-page":"532","article-title":"Formal verification of avionics software products","volume":"vol. 5850","author":"Souyris","year":"2009"},{"issue":"3","key":"10.1016\/j.scico.2015.09.006_br1210","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1016\/j.cosrev.2011.02.002","article-title":"Verification conditions for source-level imperative programs","volume":"5","author":"Frade","year":"2011","journal-title":"Comput. Sci. Rev."},{"issue":"1\u20132","key":"10.1016\/j.scico.2015.09.006_br1220","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1016\/j.jlap.2003.07.005","article-title":"Weakest pre-condition reasoning for Java programs with JML annotations","volume":"58","author":"Jacobs","year":"2004","journal-title":"J. Log. Algebr. Program."},{"key":"10.1016\/j.scico.2015.09.006_br1230","series-title":"Proceedings of the Symposium on Formal Methods Europe","first-page":"422","article-title":"Java applet correctness: a developer-oriented approach","volume":"vol. 2805","author":"Burdy","year":"2003"},{"key":"10.1016\/j.scico.2015.09.006_br1240","series-title":"Proceedings of the ACM conference on Programming Language Design and Implementation","first-page":"363","article-title":"Snugglebug: a powerful approach to weakest preconditions","author":"Chandra","year":"2009"},{"key":"10.1016\/j.scico.2015.09.006_br1250","series-title":"Proceedings of the Conference on Algebraic Methodology and Software Technology","first-page":"145","article-title":"Explaining verification conditions","volume":"vol. 5140","author":"Denney","year":"2008"},{"key":"10.1016\/j.scico.2015.09.006_br1260","series-title":"Proceedings of the Workshop on Formal Techniques for Java-like Programs","first-page":"6:1","article-title":"Strongest postcondition of unstructured programs","author":"Grigore","year":"2009"},{"issue":"4","key":"10.1016\/j.scico.2015.09.006_br1270","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1145\/115372.115320","article-title":"Efficiently computing static single assignment form and the control dependence graph","volume":"13","author":"Cytron","year":"1991","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/j.scico.2015.09.006_br1280","series-title":"Proceedings of the ACM symposium on the Principles Of Programming Languages","first-page":"193","article-title":"Avoiding exponential explosion: generating compact verification conditions","author":"Flanagan","year":"2001"},{"issue":"6","key":"10.1016\/j.scico.2015.09.006_br1290","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","article-title":"Efficient weakest preconditions","volume":"93","author":"Leino","year":"2005","journal-title":"Inf. Process. Lett."},{"key":"10.1016\/j.scico.2015.09.006_br1300","series-title":"Proceedings of Conference on Computer Aided Verification","first-page":"366","article-title":"Structural abstraction of software verification conditions","volume":"vol. 4590","author":"Babic","year":"2007"},{"key":"10.1016\/j.scico.2015.09.006_br1310","series-title":"Haifa Verification Conference","first-page":"169","article-title":"Exploiting shared structure in software verification conditions","volume":"vol. 4899","author":"Babic","year":"2007"},{"key":"10.1016\/j.scico.2015.09.006_br1320","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/360933.360975","article-title":"Guarded commands, nondeterminancy and formal derivation of programs","volume":"18","author":"Dijkstra","year":"1975","journal-title":"Commun. ACM"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S016764231500266X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S016764231500266X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,12,2]],"date-time":"2019-12-02T19:36:42Z","timestamp":1575315402000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S016764231500266X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12]]},"references-count":129,"alternative-id":["S016764231500266X"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2015.09.006","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2015,12]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Designing a verifying compiler: Lessons learned from developing Whiley","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.scico.2015.09.006","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2015 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}