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 (CASSIS 2004),
Lecture Notes in Computer Science 3362.
Springer-Verlag,
doi:10.1007/978-3-540-30569-9_3.
Bernhard Beckert, Reiner Hähnle & Peter H. Schmitt (2007):
Verification of Object-Oriented Software: The KeY Approach.
LNCS 4334.
Springer-Verlag,
doi:10.1007/978-3-540-69061-0.
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,
doi:10.1145/2489837.2489838.
Lilian Burdy, Marieke Huisman & Mariela Pavlova (2007):
Preliminary Design of BML: A Behavioral Interface Specification Language for Java Bytecode.
In: Proceedings of the 10th International Conference on Fundamental Approaches to Software Engineering,
FASE'07,
doi:10.1007/978-3-540-71289-3_18.
Patrice Chalin (2004):
JML support for primitive arbitrary precision numeric types: Definition and semantics.
Journal of Object Technology 3(6),
pp. 57–79,
doi:10.5381/jot.2004.3.6.a3.
Patrice Chalin (2005):
Reassessing JML's logical foundation.
Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP05), Glasgow, Scotland.
Patrice Chalin & Perry R James (2007):
Non-null references by default in Java: Alleviating the nullity annotation burden.
In: ECOOP 2007.
Springer,
doi:10.1007/978-3-540-73589-2_12.
Patrice Chalin, Perry R. James & Frédéric Rioux (2008):
Reducing the use of nullable types through non-null by default and monotonic non-null..
IET Software 2(6),
pp. 515–531,
doi:10.1049/iet-sen:20080010.
Jacek Chrzaszcz, Marieke Huisman & Aleksy Schubert (2009):
BML and Related Tools.
In: FrankS. Boer, MarcelloM. Bonsangue & Eric Madelaine: Formal Methods for Components and Objects,
Lecture Notes in Computer Science 5751.
Springer,
pp. 278–297,
doi:10.1007/978-3-642-04167-9_14.
David Cok (2010):
Improved usability and performance of SMT solvers for debugging specifications.
International Journal on Software Tools for Technology Transfer (STTT) 12,
doi:10.1007/s10009-010-0138-x.
David R. Cok (2004):
Reasoning with specifications containing method calls in JML and first-order provers.
In: Erik Poll: ECOOP Workshop FTfJP'2004 Formal Techniques for Java-like Programs,
pp. 41–48.
David R. Cok (2008):
Adapting JML to generic types and Java 1.6.
SAVCBS'08.
David R. Cok (2011):
jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2.
In: Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann & Rajeev Joshi: NASA Formal Methods,
Lecture Notes in Computer Science 6617.
Springer Berlin Heidelberg,
doi:10.1007/978-3-642-20398-5_36.
David R. Cok & Scott C. Johnson (2014):
SPEEDY: An Eclipse-based IDE for invariant inference.
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.
LNCS 3362.
Springer-Verlag,
doi:10.1007/b105030.
CVC4: http://cvc4.cs.nyu.edu.
Ádám Darvas & Peter Müller (2006):
Reasoning About Method Calls in Interface Specifications.
Journal of Object Technology 5(5),
pp. 59–85,
doi:10.5381/jot.2006.5.5.a3.
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.
Werner Dietl, Sophia Drossopoulou & Peter Müller (2007):
Generic Universe Types.
In: Erik Ernst: ECOOP,
Lecture Notes in Computer Science 4609.
Springer,
pp. 28–53,
doi:10.1007/978-3-540-73589-2_3.
Michael D. Ernst (2011):
Type Annotations specification (JSR 308).
http://types.cs.washington.edu/jsr308/.
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, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe & Raymie Stata (2002):
Extended Static Checking for Java.
In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation,
PLDI '02.
ACM,
New York, NY, USA,
pp. 234–245,
doi:10.1145/512529.512558.
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/.
Claire Le Goues, K. Rustan M. Leino & MichałMoskal (2011):
The Boogie Verification Debugger (Tool Paper).
In: Gilles Barthe, Alberto Pardo & Gerardo Schneider: Software Engineering and Formal Methods — 9th International Conference, SEFM 2011,
Lecture Notes in Computer Science 7041.
Springer,
pp. 407–414,
doi:10.1007/978-3-642-24690-6_28.
Gary T. Leavens, Albert L. Baker & Clyde Ruby (1999):
JML: A Notation for Detailed Design.
In: Haim Kilov, Bernhard Rumpe & Ian Simmonds: Behavioral Specifications of Businesses and Systems.
Kluwer Academic Publishers,
Boston,
pp. 175–188,
doi:10.1007/978-1-4615-5229-1_12.
Gary T. Leavens & David R. Cok (2005):
Adapting Observational Purity to JML.
Presented at IFIP WG 2.3.
Gary T. Leavens & Peter Müller (2006):
Information Hiding and Visibility in Interface Specifications.
Technical Report 06-28.
Department of Computer Science, Iowa State University,
Ames, Iowa.
Available at ftp://ftp.cs.iastate.edu/pub/techreports/TR06-28/TR.pdf.
In ICSE 2007, pages 385-395..
Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David R. Cok, Peter Müller, Joseph Kiniry, Patrice Chalin & Daniel M. Zimmerman (2008):
JML Reference Manual.
Available from http://www.jmlspecs.org.
K. Rustan M. Leino (1998):
Data Groups: Specifying the Modification of Extended State.
In: Proceedings of the 13th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications,
OOPSLA '98.
ACM,
doi:10.1145/286942.286953.
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 (2010):
Dafny: An Automatic Program Verifier for Functional Correctness.
In: Edmund M. Clarke & Andrei Voronkov: LPAR-16,
Lecture Notes in Computer Science 6355,
doi:10.1007/978-3-642-17511-4_20.
K. Rustan M. Leino & Peter Müller (2006):
A verification methodology for model fields.
In: Peter Sestoft: European Symposium on Programming (ESOP),
Lecture Notes in Computer Science 3924.
Springer-Verlag,
pp. 115–130,
doi:10.1007/11693024_9.
K. Rustan M. Leino & Valentin Wüstholz (2014):
The Dafny Integrated Development Environment.
Electronic Proceedings in Theoretical Computer Science (EPTCS).
To appear..
Bertrand Meyer (1988):
Object-oriented Software Construction.
Prentice Hall,
New York, NY.
Matthew M. Papi, Mahmood Ali, Telmo Luis Correa Jr., Jeff H. Perkins & Michael D. Ernst (2008):
Practical pluggable types for Java.
In: ISSTA,
pp. 201–212,
doi:10.1145/1390630.1390656.
Steve M. Shaner, Gary T. Leavens & David A. Naumann (2007):
Modular verification of higher-order methods with mandatory calls specified by model programs.
In: OOPSLA,
doi:10.1145/1297027.1297053.
Daniel M. Zimmerman & Rinkesh Nagmoti (2011):
JMLUnit: The Next Generation.
In: Bernhard Beckert & Claude Marché: Formal Verification of Object-Oriented Software,
Lecture Notes in Computer Science 6528.
Springer,
pp. 183–197,
doi:10.1007/978-3-642-18070-5_13.
ACSL web site. http://www.frama-c.cea.fr/acsl.html.