References

  1. Michael Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs & K. Rustan M. Leino (2005): Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf & Willem P. de Roever: Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures, Lecture Notes in Computer Science 4111. Springer, pp. 364–387, doi:10.1007/11804192_17.
  2. Clark Barrett, Aaron Stump & Cesare Tinelli (2010): The SMT-LIB Standard Version 2.0. SMT-LIB.org. Available at http://SMT-LIB.org.
  3. Jens Bendisposto, Sebastian Krings & Michael Leuschel (2014): Who watches the watchers: Validating the ProB Validation Tool. In: Dubois, pp. 16–29, doi:10.4204/EPTCS.149.3.
  4. Patrice Chalin, Perry R. James & George Karabotsos (2008): JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML. In: Natarajan Shankar & Jim Woodcock: Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings, Lecture Notes in Computer Science 5295. Springer, pp. 70–83, doi:10.1007/978-3-540-87873-5_9.
  5. David R. Cok (2014): OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Dubois, pp. 79–92, doi:10.4204/EPTCS.149.8.
  6. David R. Cok & Scott C. Johnson (2014): SPEEDY: An Eclipse-based IDE for invariant inference. In: Dubois, pp. 44–57, doi:10.4204/EPTCS.149.5.
  7. Charles T. Cook, Svetlana Drachova-Strang, Yu-Shan Sun, Murali Sitaraman, Jeffrey C. Carver & Joseph E. Hollingsworth (2013): Specification and reasoning in SE projects using a Web IDE. In: Tony Cowling, Shawn Bohner & Mark A. Ardis: 26th International Conference on Software Engineering Education and Training, CSEE&T 2013, San Francisco, CA, USA, May 19-21, 2013. IEEE, pp. 229–238, doi:10.1109/CSEET.2013.6595254.
  8. Charles T. Cook, Heather K. Harton, Hampton Smith & Murali Sitaraman (2012): Specification engineering and modular verification using a web-integrated verifying compiler. In: Martin Glinz, Gail C. Murphy & Mauro Pezzè: 34th International Conference on Software Engineering, ICSE 2012, June 2-9, 2012, Zurich, Switzerland. IEEE, pp. 1379–1382, doi:10.1109/ICSE.2012.6227243.
  9. Charles T. Cook, Yu-Shan Sun & Murali Sitaraman (2015): Experience report: evolution of a web-integrated software development and verification environment. Softw., Pract. Exper. 45(6), pp. 857–872, doi:10.1002/spe.2259.
  10. David Detlefs, Greg Nelson & James B. Saxe (2005): Simplify: a theorem prover for program checking. J. ACM 52(3), pp. 365–473, doi:10.1145/1066100.1066102.
  11. Svetlana Drachova-Strang (2013): Teaching and Assessment of Mathematical Principles for Software Correctness Using a Reasoning Concept Inventory. Clemson University. Available at http://www.cs.clemson.edu/resolve/research/docs/Dissertation-Drachova-Strang.pdf.
  12. Svetlana Drachova-Strang, Jason Hallstrom, Murali Sitaraman, Joe Hollingsworth & Joan Krone (2015): Teaching Mathematical Reasoning Principles for Software Correctness and its Assessment. ACM Transactions on Computing Education, pp. accepted, to appear.
  13. Catherine Dubois, Dimitra Giannakopoulou & Dominique Méry (2014): Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, April 6, 2014. EPTCS 149, doi:10.4204/EPTCS.149.
  14. Carlo A. Furia, Julian Tschannen & Bertrand Meyer (2014): The Gotthard Approach: Designing an Integrated Verification Environment for Eiffel. In: Dubois, pp. 1–2, doi:10.4204/EPTCS.149. Abstract of invited talk.
  15. Heather Harton (2011): Mechanical and Modular Verification Condition Generation For Object-Based Software. Clemson University. Available at http://www.cs.clemson.edu/resolve/research/docs/Dissertation-Harton_2_1.pdf.
  16. John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller & Matthew J. Parkinson (2012): Behavioral interface specification languages. ACM Comput. Surv. 44(3), pp. 16, doi:10.1145/2187671.2187678.
  17. Bart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx & Frank Piessens (2011): VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In: Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann & Rajeev Joshi: NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings, Lecture Notes in Computer Science 6617. Springer, pp. 41–55, doi:10.1007/978-3-642-20398-5_4.
  18. Mathieu Jaume & Théo Laurent (2014): Teaching Formal Methods and Discrete Mathematics. In: Dubois, pp. 30–43, doi:10.4204/EPTCS.149.4.
  19. Jason Kirschenbaum & Bruce M. Adcock (2009): Verifying Component-Based Software: Deep Mathematics or Simple Bookkeeping?. In: Stephen H. Edwards & Gregory Kulczycki: Formal Foundations of Reuse and Domain Engineering, 11th International Conference on Software Reuse, ICSR 2009, Falls Church, VA, USA, September 27-30, 2009. Proceedings, Lecture Notes in Computer Science 5791. Springer, pp. 31–40, doi:10.1007/978-3-642-04211-9_4.
  20. Gregory Kulczycki & Murali Sitaraman (2013): A Language for Building Verified Software Components. In: John M. Favaro & Maurizio Morisio: Safe and Secure Software Reuse - 13th International Conference on Software Reuse, ICSR 2013, Pisa, Italy, June 18-20. Proceedings, Lecture Notes in Computer Science 7925. Springer, pp. 308–314, doi:10.1007/978-3-642-38977-1_23.
  21. Gregory W. Kulczycki (2004): Direct Reasoning. Clemson University. Available at http://www.nvc.vt.edu/gregwk/assets/research-papers/kulczycki04direct.pdf.
  22. Gary T. Leavens, Albert L. Baker & Clyde Ruby (2006): Preliminary design of JML: a behavioral interface specification language for java. ACM SIGSOFT Software Engineering Notes 31(3), pp. 1–38, doi:10.1145/1127878.1127884.
  23. K. Rustan M. Leino (2010): Dafny: An Automatic Program Verifier for Functional Correctness. In: Edmund M. Clarke & Andrei Voronkov: Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers, Lecture Notes in Computer Science 6355. Springer, pp. 348–370, doi:10.1007/978-3-642-17511-4_20.
  24. K. Rustan M. Leino & Valentin Wüstholz (2014): The Dafny Integrated Development Environment. In: Dubois, pp. 3–15, doi:10.4204/EPTCS.149.2.
  25. Bertrand Meyer (1988): Eiffel: A language and environment for software engineering. Journal of Systems and Software 8(3), pp. 199–246, doi:10.1016/0164-1212(88)90022-2.
  26. Bertrand Meyer (1997): Object-Oriented Software Construction, 2nd Edition. Prentice-Hall.
  27. Leonardo Mendonça de Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In: C. R. Ramakrishnan & Jakob Rehof: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Lecture Notes in Computer Science 4963. Springer, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  28. Greg Nelson & Derek C. Oppen (1980): Fast Decision Procedures Based on Congruence Closure. J. ACM 27(2), pp. 356–364, doi:10.1145/322186.322198.
  29. Tobias Nipkow, Lawrence C. Paulson & Markus Wenzel (2002): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science 2283. Springer, doi:10.1007/3-540-45949-9.
  30. François Pessaux (2014): FoCaLiZe: Inside an F-IDE. In: Dubois, pp. 64–78, doi:10.4204/EPTCS.149.7.
  31. Murali Sitaraman & Bruce M. Adcock (2011): Building a push-button RESOLVE verifier: Progress and challenges. Formal Asp. Comput. 23(5), pp. 607–626, doi:10.1007/s00165-010-0154-3.
  32. Murali Sitaraman & Bruce Weide (1994): Component-based Software Using RESOLVE. SIGSOFT Software Engineering Notes 19(4), pp. 21–22, doi:10.1145/190679.199221.
  33. Jan Smans, Bart Jacobs & Frank Piessens (2013): VeriFast for Java: A Tutorial. In: Dave Clarke, James Noble & Tobias Wrigstad: Aliasing in Object-Oriented Programming. Types, Analysis and Verification, Lecture Notes in Computer Science 7850. Springer, pp. 407–442, doi:10.1007/978-3-642-36946-9_14.
  34. Hampton Smith (2013): Engineering Specifications and Mathematics for Verified Software. Clemson University. Available at http://www.cs.clemson.edu/resolve/research/docs/Dissertation-Smith.pdf.
  35. Julian Tschannen, Carlo A. Furia, Martin Nordio & Bertrand Meyer (2011): Verifying Eiffel Programs with Boogie. CoRR abs/1106.4700. Available at http://arxiv.org/abs/1106.4700.
  36. Daniel Welch, Charles T. Cook, Yu-Shan Sun & Murali Sitaraman (2014): A web-integrated verifying compiler for RESOLVE: a research perspective. In: Dharanipragada Janakiram, Koushik Sen & Vinay Kulkarni: 7th India Software Engineering Conference, Chennai, ISEC '14, Chennai, India - February 19 - 21, 2014. ACM, pp. 12:1–12:6, doi:10.1145/2590748.2590760.
  37. John Witulski & Michael Leuschel (2014): Checking Computations of Formal Method Tools - A Secondary Toolchain for ProB. In: Dubois, pp. 93–105, doi:10.4204/EPTCS.149.9.

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