Mike Barnett & K. Rustan M. Leino (2005):
Weakest-precondition of unstructured programs.
In: Michael D. Ernst & Thomas P. Jensen: Program Analysis For Software Tools and Engineering (PASTE).
ACM,
doi:10.1145/1108792.1108813.
Mike Barnett, K. Rustan M. Leino & Wolfram Schulte (2005):
The Spec# Programming System: An Overview.
In: Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet & Traian Muntean: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices,
Lecture Notes in Computer Science 3362.
Springer Berlin Heidelberg,
pp. 49–69,
doi:10.1007/978-3-540-30569-9_3.
Clark Barrett, Aaron Stump & Cesare Tinelli (2010):
The SMT-LIB Standard: Version 2.0.
Technical Report.
Department of Computer Science, The University of Iowa.
Available at http://www.SMT-LIB.org.
Clark Barrett, Aaron Stump & Cesare Tinelli (2010):
The SMT-LIB Standard: Version 2.0.
In: A. Gupta & D. Kroening: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, England).
Available at http://www.smt-lib.org.
P. Baudin:
ACSL: ANSI C Specification Language.
http://frama-c.com/download/acsl_1.4.pdf.
Bernhard Beckert, Reiner Hähnle & Peter H. Schmitt (2007):
Verification of object-oriented software : The KeY Approach.
Springer,
doi:10.1007/978-3-540-69061-0.
Yves Bertot & Pierre Castéran (2004):
Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions.
Texts in theoretical computer science.
Springer,
Berlin, New York,
doi:10.1007/978-3-662-07964-5.
Available at http://opac.inria.fr/record=b1101046.
Régis Blanc, Viktor Kuncak, Etienne Kneuss & Philippe Suter (2013):
An Overview of the Leon Verification System: Verification by Translation to Recursive Functions.
In: Proceedings of the 4th Workshop on Scala,
SCALA '13.
ACM,
New York, NY, USA,
pp. 1:1–1:10,
doi:10.1145/2489837.2489838.
Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino & Erik Poll (2003):
An overview of JML tools and applications.
In: Thomas Arts & Wan Fokkink: Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03),
Electronic Notes in Theoretical Computer Science (ENTCS) 80.
Elsevier,
pp. 73–89,
doi:10.1016/S1571-0661(04)80810-7.
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: Stefan Berghofer, Tobias Nipkow, Christian Urban & Makarius Wenzel: Theorem Proving in Higher Order Logics,
Lecture Notes in Computer Science 5674.
Springer Berlin Heidelberg,
pp. 23–42,
doi:10.1007/978-3-642-03359-9_2.
David R. Cok (2011):
jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2.
In: Mihaela Bobaru, Klaus Havelund, GerardJ. Holzmann & Rajeev Joshi: NASA Formal Methods,
Lecture Notes in Computer Science 6617.
Springer Berlin Heidelberg,
pp. 480–486,
doi:10.1007/978-3-642-20398-5_36.
David R. Cok (2011):
OpenJML: JML for Java 7 by Extending OpenJDK.
In: Mihaela Bobaru, Klaus Havelund, GerardJ. Holzmann & Rajeev Joshi: NASA Formal Methods,
Lecture Notes in Computer Science 6617.
Springer Berlin Heidelberg,
pp. 472–479,
doi:10.1007/978-3-642-20398-5_35.
David R. Cok (2014):
OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse.
Electronic Proceedings in Theoretical Computer Science (EPTCS).
To appear..
David R. Cok & Joseph R. Kiniry (2005):
ESC/Java2: Uniting ESC/Java and JML: Progress and issues in building and using ESC/Java2, including a case study involving the use of the tool to verify portions of an Internet voting tally system.
In: Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet & Traian Muntean: Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS 2004),
Lecture Notes in Computer Science 3362.
Springer-Verlag,
pp. 108–128,
doi:10.1007/b105030.
CVC4: http://cvc4.cs.nyu.edu.
Leonardo De Moura & Nikolaj Bjørner (2008):
Z3: An Efficient SMT Solver.
In: Proceedings of the Theory and Practice of Software,
TACAS'08/ETAPS'08.
Springer-Verlag,
Berlin, Heidelberg,
pp. 337–340.
Available at http://portal.acm.org/citation.cfm?id=1792734.1792766.
Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz & Chen Xiao (2007):
The Daikon system for dynamic detection of likely invariants.
Science of Computer Programming 69(1–3),
pp. 35–45,
doi:10.1016/j.scico.2007.01.015.
Jean-Christophe Filliâtre & Andrei Paskevich (2013):
Why3 — Where Programs Meet Provers.
In: Matthias Felleisen & Philippa Gardner: Programming Languages and Systems,
Lecture Notes in Computer Science 7792.
Springer Berlin Heidelberg,
pp. 125–128,
doi:10.1007/978-3-642-37036-6_8.
Cormac Flanagan & James B. Saxe (2001):
Avoiding exponential explosion: generating compact verification conditions.
SIGPLAN Not. 36(3),
pp. 193–205,
doi:10.1145/373243.360220.
Frama-C: http://frama-c.com/.
L. Paulson (1994):
Isabelle: A Generic Theorem Prover.
Lecture Notes in Computer Science 828.
Springer-Verlag,
doi:10.1007/BFb0030541.
K. Rustan M. Leino (2005):
Efficient weakest preconditions.
Inf. Process. Lett. 93(6),
pp. 281–288,
doi:10.1016/j.ipl.2004.10.015.
K. Rustan M. Leino & Valentin Wüstholz (2014):
The Dafny Integrated Development Environment.
Electronic Proceedings in Theoretical Computer Science (EPTCS).
To appear..
S. Owre, J. M. Rushby & N. Shankar (1992):
PVS: A Prototype Verification System.
In: Deepak Kapur: 11th International Conference on Automated Deduction (CADE),
Lecture Notes in Artificial Intelligence 607.
Springer-Verlag,
Saratoga, NY,
pp. 748–752,
doi:10.1007/3-540-55602-8_217.
Available at http://www.csl.sri.com/papers/cade92-pvs/.
Todd W. Schiller & Michael D. Ernst (2012):
Reducing the barriers to writing verified specifications.
In: Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2012),
Tucson, AZ, USA,
pp. 95–112.
Available at http://doi.acm.org/10.1145/2384616.2384624.
SWIG: http://www.swig.org.
CodeSonar web site. http://www.grammatech.com/products/codesonar.