Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reiner Hähnle, Peter H Schmitt & Mattias Ulbrich (2016):
Deductive Software Verification–The KeY Book: From Theory to Practice.
Springer,
doi:10.1007/978-3-319-49812-6.
Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte & Herman Venter (2011):
Specification and Verification: The Spec# Experience.
Comm. ACM 54,
pp. 81–91,
doi:10.1145/1953122.1953145.
Christoph Baumann, Bernhard Beckert, Holger Blasum & Thorsten Bormer (2012):
Lessons Learned from Microkernel Verification–Specification is the new Bottleneck.
SSV,
doi:10.4204/EPTCS.102.4.
Bernhard Beckert, Thorsten Bormer & Daniel Grahl (2016):
Deductive Verification of Legacy Code.
In: Proc. Int'l Symposium Leveraging Applications of Formal Methods, Verification and Validation (ISoLA).
Springer,
pp. 749–765,
doi:10.1007/978-3-319-47166-2_53.
Bernhard Beckert, Reiner Hähnle & Peter Schmitt (2007):
Verification of Object-Oriented Software: The KeY Approach.
Springer,
Berlin, Heidelberg.
Bernhard Beckert, Jonas Schiffl, Peter H Schmitt & Mattias Ulbrich (2017):
Proving JDK’s Dual Pivot Quicksort Correct.
In: Working Conference on Verified Software: Theories, Tools, and Experiments.
Springer,
pp. 35–48,
doi:10.1007/978-3-319-47846-3_5.
Yves Bertot & Pierre Castéran (2004):
Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions.
Springer,
Berlin, Heidelberg,
doi:10.1007/978-3-662-07964-5.
Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino & Jay Lorch (2017):
Everest: Towards a Verified, Drop-in Replacement of HTTPS.
In: Leibniz International Proceedings in Informatics (LIPIcs) 71.
Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik,
doi:10.4230/LIPIcs.SNAPL.2017.1.
Jonathan Bowen & Victoria Stavridou (1993):
Safety-critical Systems, Formal Methods and Standards.
Software Engineering Journal 8(4),
pp. 189–209,
doi:10.1049/sej.1993.0025.
Hagen Buchwald & Florian Meyerer (2013):
C4J: Contracts, Java und Eclipse.
Eclipse Magazin 13(3),
pp. 64–69.
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph Kiniry, Gary T. Leavens, K. Rustan M. Leino & Erik Poll (2005):
An Overview of JML Tools and Applications.
Int'l J. Software Tools for Technology Transfer (STTT) 7(3),
pp. 212–232,
doi:10.1007/s10009-004-0167-4.
Edmund M. Clarke, Orna Grumberg & Doron A. Peled (1999):
Model Checking.
MIT Press,
Cambridge, Massachussetts.
Edmund M Clarke & Jeannette M Wing (1996):
Formal methods: State of the Art and Future Directions.
ACM Computing Surveys (CSUR) 28(4),
pp. 626–643,
doi:10.1145/242223.242257.
Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, MichałMoskal, Thomas Santen, Wolfram Schulte & Stephan Tobies (2009):
VCC: A Practical System for Verifying Concurrent C.
In: Proc. Int'l. Conf. Theorem Proving in Higher Order Logics (TPHOLs).
Springer,
pp. 23–42,
doi:10.1007/978-3-540-74591-4_15.
David R. Cok (2011):
OpenJML: JML for Java 7 by Extending OpenJDK.
In: Proc. Int'l Conf. NASA Formal Methods (NFM).
Springer,
Berlin, Heidelberg,
pp. 472–479,
doi:10.1007/978-3-642-18070-5_13.
David R Cok & Joseph Kiniry (2004):
ESC/Java2: Uniting ESC/Java and JML.
In: Proc. Int'l Conf. Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS) 3362.
Springer,
pp. 108–128,
doi:10.1007/978-3-540-30569-9_6.
Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles & Boris Yakobowski (2012):
Frama-C.
In: Proc. Int'l. Conf. Software Engineering and Formal Methods (SEFM).
Springer,
pp. 233–247,
doi:10.1007/978-3-642-33826-7_16.
Stijn De Gouw, Jurriaan Rot, Frank S de Boer, Richard Bubel & Reiner Hähnle (2015):
OpenJDK’s Java.utils.Collection.sort() is Broken: The Good, the Bad and the Worst Case.
In: Proc. Int'l Conf. Computer Aided Verification (CAV).
Springer,
pp. 273–289,
doi:10.1007/978-3-319-21690-4_16.
Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn, Dominik Haneberg & Wolfgang Reif (2015):
KIV: Overview and VerifyThis Competition.
Int'l J. Software Tools for Technology Transfer (STTT) 17(6),
pp. 677–694,
doi:10.1007/s10009-014-0308-3.
H-Christian Estler, Carlo A Furia, Martin Nordio, Marco Piccioni & Bertrand Meyer (2014):
Contracts in Practice.
In: International Symposium on Formal Methods.
Springer,
pp. 230–246,
doi:10.1007/978-3-319-06410-9_17.
Jean-Christophe Filliâtre & Claude Marché (2007):
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification.
In: Computer Aided Verification.
Springer,
Berlin, Heidelberg,
pp. 173–177,
doi:10.1007/978-3-540-73368-3_21.
Robert W. Floyd (1967):
Assigning Meanings to Programs.
Mathematical Aspects of Computer Science 19,
pp. 19–32,
doi:10.1090/psapm/019/0235771.
Carlo A Furia, Martin Nordio, Nadia Polikarpova & Julian Tschannen (2017):
AutoProof: Auto-Active Functional Verification of Object-Oriented Programs.
Int'l J. Software Tools for Technology Transfer (STTT) 19(6),
pp. 697–716,
doi:10.1007/s10009-016-0419-0.
John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller & Matthew Parkinson (2012):
Behavioral Interface Specification Languages.
ACM Computing Surveys 44(3),
pp. 16:1–16:58,
doi:10.1145/2187671.2187678.
Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R Lorch, Bryan Parno, Michael L Roberts, Srinath Setty & Brian Zill (2015):
IronFleet: Proving Practical Distributed Systems Correct.
In: Proc. Symposium on Operating Systems Principles (SOSP).
ACM,
pp. 1–17,
doi:10.1145/2815400.2815428.
Chris Hawblitzel, Jon Howell, Jacob R Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang & Brian Zill (2014):
Ironclad Apps: End-to-End Security via Automated Full-System Verification.
In: Proc. USENIX Symposium Operating Systems Design and Implementation (OSDI) 14,
pp. 165–181.
C. A. R. Hoare (2003):
The Verifying Compiler: A Grand Challenge for Computing Research.
In: Proc. Joint Modular Languages Conference (JMLC).
Springer,
Berlin, Heidelberg,
pp. 25–35,
doi:10.1007/978-3-540-45213-3_4.
Robert Kaiser & Stephan Wagner (2007):
Evolution of the PikeOS Microkernel.
In: Proc. Int'l. Workshop on Microkernels for Embedded Systems (MIKES),
pp. 50.
John C Knight, Colleen L DeJong, Matthew S Gibble & Luis G Nakano (1997):
Why are Formal Methods not used more Widely?.
In: Fourth NASA Langley Formal Methods Workshop.
Citeseer,
doi:10.1.1.2.3395.
Alexander Knüppel, Thomas Thüm, Carsten I. Pardylla & Ina Schaefer (2018):
Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY.
In: Proc. Int'l. Conf. Interactive Theorem Proving (ITP).
Springer,
doi:10.1007/978-3-642-29044-2.
Ralf Küesters, Tomasz Truderung & Andreas Vogt (2011):
Verifiability, Privacy, and Coercion-resistance: New Insights From a Case Study.
In: Proc. Symposium on Security and Privacy (SP).
IEEE,
pp. 538–553,
doi:10.1109/SP.2011.21.
Gary T. Leavens & Peter Müller (2007):
Information Hiding and Visibility in Interface Specifications.
In: Proc. Int'l Conf. Software Engineering (ICSE).
IEEE,
Washington, DC, USA,
pp. 385–395,
doi:10.1109/ICSE.2007.44.
Gary T Leavens & David A Naumann (2006):
Behavioral Subtyping is Equivalent to Modular Reasoning for Object-oriented Programs.
Barbara Liskov & John Guttag (1986):
Abstraction and Specification in Program Development.
MIT Press,
Cambridge, MA, USA.
Barbara H. Liskov & Jeannette M. Wing (1994):
A Behavioral Notion of Subtyping.
ACM Trans. Programming Languages and Systems (TOPLAS) 16(6),
pp. 1811–1841,
doi:10.1145/197320.197383.
Claude Marché & Yannick Moy (2012):
The Jessie Plugin for Deductive Verification in Frama-C.
INRIA Saclay Île-de-France and LRI, CNRS UMR,
doi:10.1.1.229.3233.
Bertrand Meyer (1988):
Object-Oriented Software Construction,
1st edition.
Prentice-Hall, Inc.,
Upper Saddle River, NJ, USA.
Bertrand Meyer (1992):
Applying Design by Contract.
IEEE Computer 25(10),
pp. 40–51,
doi:10.1109/2.161279.
Tobias Nipkow, Markus Wenzel & Lawrence C. Paulson (2002):
Isabelle/HOL: A Proof Assistant for Higher-Order Logic.
Springer,
Berlin, Heidelberg,
doi:10.1007/3-540-45949-9.
Sam Owre, Sreeranga P. Rajan, John M. Rushby, Natarajan Shankar & Mandayam K. Srivas (1996):
PVS: Combining Specification, Proof Checking, and Model Checking.
In: Proc. Int'l Conf. Computer Aided Verification (CAV).
Springer,
Berlin, Heidelberg,
pp. 411–414,
doi:10.1007/3-540-61474-5_91.
Dillon Pariente & Emmanuel Ledinot (2010):
Formal Verification of Industrial C Code using Frama-C: A Case Study.
Proc. Int'l Conf. Formal Verification of Object-Oriented Software (FoVeOOS),
pp. 205.
Nadia Polikarpova, Julian Tschannen & Carlo A Furia (2015):
A Fully Verified Container Library.
In: Proc. Int'l Symposium Formal Methods (FM).
Springer,
pp. 414–434,
doi:10.1007/978-3-319-19249-9_26.
Robby, Edwin Rodríguez, Matthew B. Dwyer & John Hatcliff (2006):
Checking JML Specifications Using an Extensible Software Model Checking Framework.
Int'l J. Software Tools for Technology Transfer (STTT) 8(3),
pp. 280–299,
doi:10.1007/s10009-005-0218-5.
Hartley Rogers & H Rogers (1967):
Theory of Recursive Functions and Effective Computability 5.
McGraw-Hill New York.
John Rushby (1997):
Formal Methods and their role in the Certification of Critical Systems.
In: Safety and Reliability of Software Based Systems.
Springer,
pp. 1–42,
doi:10.1007/978-1-4471-0921-1_1.
Donald Sannella (1988):
A Survey of Formal Software Development Methods.
University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Science.
Johann Schumann (2001):
Automated Theorem Proving in Software Engineering.
Springer,
Berlin, Heidelberg,
doi:10.1007/978-3-662-22646-9.
Johann M Schumann (2001):
Automated Theorem Proving in Software Engineering.
Springer Science & Business Media,
doi:10.1007/978-3-662-22646-9.
Thomas Thüm, Ina Schaefer, Martin Kuhlemann & Sven Apel (2011):
Proof Composition for Deductive Verification of Software Product Lines.
In: Proc. Int'l Workshop Variability-intensive Systems Testing, Validation and Verification (VAST).
IEEE,
Washington, DC, USA,
pp. 270–277,
doi:10.1109/ICSTW.2011.48.
Dean Wampler (2006):
Contract4J for Design by Contract in Java: Design Pattern-like Protocols and Aspect Interfaces.
In: Fifth AOSD Workshop on ACP4IS,
pp. 27–30,
doi:10.1.1.115.2281.
Why Development Team:
Why: A Software Verification Platform.
Website.
Available online at http://why.lri.fr/.