References

  1. Alt-ergo: http://alt-ergo.lri.fr/.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. P. Baudin: ACSL: ANSI C Specification Language. http://frama-c.com/download/acsl_1.4.pdf.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. Clang: http://clang.llvm.org/.
  12. CodeSurfer: http://www.grammatech.com/research/technologies/codesurfer.
  13. 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.
  14. 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.
  15. 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.
  16. David R. Cok (2014): OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. Electronic Proceedings in Theoretical Computer Science (EPTCS). To appear..
  17. 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.
  18. CVC4: http://cvc4.cs.nyu.edu.
  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. 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.
  22. 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.
  23. 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.
  24. Frama-C: http://frama-c.com/.
  25. L. Paulson (1994): Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science 828. Springer-Verlag, doi:10.1007/BFb0030541.
  26. K. Rustan M. Leino (2005): Efficient weakest preconditions. Inf. Process. Lett. 93(6), pp. 281–288, doi:10.1016/j.ipl.2004.10.015.
  27. 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. Springer, pp. 348–370, doi:10.1007/978-3-642-17511-4_20. Available at http://dl.acm.org/citation.cfm?id=1939141.1939161.
  28. 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.
  29. K. Rustan M. Leino & Valentin Wüstholz (2014): The Dafny Integrated Development Environment. Electronic Proceedings in Theoretical Computer Science (EPTCS). To appear..
  30. 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/.
  31. Sam Owre, Natarajan Shankar, John M. Rushby & David W. J. Stringer-Calvert (2001): PVS Language Reference. SRI International. Available at http://pvs.csl.sri.com/doc/pvs-language-reference.pdf. Version 2.4.
  32. 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.
  33. SWIG: http://www.swig.org.
  34. CodeSonar web site. http://www.grammatech.com/products/codesonar.
  35. JML web site. http://www.jmlspecs.org.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org