References

  1. 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.
  2. 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.
  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.
  4. 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.
  5. 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.
  6. 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.
  7. Patrice Chalin (2005): Reassessing JML's logical foundation. Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP05), Glasgow, Scotland.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. David R. Cok (2008): Adapting JML to generic types and Java 1.6. SAVCBS'08.
  14. 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.
  15. David R. Cok & Scott C. Johnson (2014): SPEEDY: An Eclipse-based IDE for invariant inference. Electronic Proceedings in Theoretical Computer Science (EPTCS). To appear..
  16. 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.
  17. CVC4: http://cvc4.cs.nyu.edu.
  18. Á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.
  19. 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.
  20. David Detlefs, Greg Nelson & James B. Saxe (2003): Simplify: A Theorem Prover for Program Checking. Technical Report HPL-2003-148. HP Labs. Available at http://www.hpl.hp.com/techreports/2003/HPL-2003-148.pdf.
  21. 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.
  22. Michael D. Ernst (2011): Type Annotations specification (JSR 308). http://types.cs.washington.edu/jsr308/.
  23. 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.
  24. 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.
  25. 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.
  26. 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.
  27. Frama-C: http://frama-c.com/.
  28. 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.
  29. 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.
  30. Gary T. Leavens & David R. Cok (2005): Adapting Observational Purity to JML. Presented at IFIP WG 2.3.
  31. 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..
  32. 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.
  33. 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.
  34. K. Rustan M. Leino (2005): Efficient weakest preconditions. Inf. Process. Lett. 93(6), pp. 281–288, doi:10.1016/j.ipl.2004.10.015.
  35. 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.
  36. 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.
  37. K. Rustan M. Leino, Greg Nelson & James B. Saxe (2000): ESC/Java User's Manual. Technical Note. Compaq Systems Research Center. Available at http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-TN-2000-002.pdf?jumpid=reg_R1002_USEN.
  38. K. Rustan M. Leino & Valentin Wüstholz (2014): The Dafny Integrated Development Environment. Electronic Proceedings in Theoretical Computer Science (EPTCS). To appear..
  39. Bertrand Meyer (1988): Object-oriented Software Construction. Prentice Hall, New York, NY.
  40. Mobius. http://software.imdea.org/~gbarthe/mobius/bin/view/Mobius/WebHome.html.
  41. 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.
  42. 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.
  43. 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.
  44. ACSL web site. http://www.frama-c.cea.fr/acsl.html.
  45. JML web site. http://www.jmlspecs.org.
  46. OpenJDK web site. http://openjdk.java.net.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org