References

  1. 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.
  2. 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.
  3. 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.
  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.
  5. Bernhard Beckert, Reiner Hähnle & Peter Schmitt (2007): Verification of Object-Oriented Software: The KeY Approach. Springer, Berlin, Heidelberg.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. Hagen Buchwald & Florian Meyerer (2013): C4J: Contracts, Java und Eclipse. Eclipse Magazin 13(3), pp. 64–69.
  11. 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.
  12. Edmund M. Clarke, Orna Grumberg & Doron A. Peled (1999): Model Checking. MIT Press, Cambridge, Massachussetts.
  13. 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.
  14. 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.
  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.
  16. 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.
  17. 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.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. Robert W. Floyd (1967): Assigning Meanings to Programs. Mathematical Aspects of Computer Science 19, pp. 19–32, doi:10.1090/psapm/019/0235771.
  23. 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.
  24. 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.
  25. 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.
  26. 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.
  27. 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.
  28. Robert Kaiser & Stephan Wagner (2007): Evolution of the PikeOS Microkernel. In: Proc. Int'l. Workshop on Microkernels for Embedded Systems (MIKES), pp. 50.
  29. 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.
  30. 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.
  31. 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.
  32. Gary T. Leavens & Yoonsik Cheon (2006): Design by Contract with JML. Available at http://www.jmlspecs.org/jmldbc.pdf.
  33. 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.
  34. Gary T Leavens & David A Naumann (2006): Behavioral Subtyping is Equivalent to Modular Reasoning for Object-oriented Programs.
  35. Barbara Liskov & John Guttag (1986): Abstraction and Specification in Program Development. MIT Press, Cambridge, MA, USA.
  36. 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.
  37. 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.
  38. Bertrand Meyer (1988): Object-Oriented Software Construction, 1st edition. Prentice-Hall, Inc., Upper Saddle River, NJ, USA.
  39. Bertrand Meyer (1992): Applying Design by Contract. IEEE Computer 25(10), pp. 40–51, doi:10.1109/2.161279.
  40. 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.
  41. 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.
  42. 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.
  43. 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.
  44. 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.
  45. Hartley Rogers & H Rogers (1967): Theory of Recursive Functions and Effective Computability 5. McGraw-Hill New York.
  46. 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.
  47. Donald Sannella (1988): A Survey of Formal Software Development Methods. University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Science.
  48. Johann Schumann (2001): Automated Theorem Proving in Software Engineering. Springer, Berlin, Heidelberg, doi:10.1007/978-3-662-22646-9.
  49. Johann M Schumann (2001): Automated Theorem Proving in Software Engineering. Springer Science & Business Media, doi:10.1007/978-3-662-22646-9.
  50. 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.
  51. 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.
  52. Why Development Team: Why: A Software Verification Platform. Website. Available online at http://why.lri.fr/.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org