Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi\'c, Tim King, Andrew Reynolds & Cesare Tinelli (2011):
CVC4.
In: Computer Aided Verification,
Lecture Notes in Computer Science 6806.
Springer,
pp. 171–177,
doi:10.1007/978-3-642-22110-1_14.
Benedikt Becker, Cláudio Belo Lourenço & Claude Marché (2021):
Giant-step Semantics for the Categorisation of Counterexamples.
Research Report RR-9407.
Inria.
Available at https://hal.inria.fr/hal-03213438.
François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala, Stéphane Lescuyer & Alain Mebsout (2008):
The Alt-Ergo Automated Theorem Prover.
http://alt-ergo.lri.fr/.
François Bobot, Jean-Christophe Filliâtre, Claude Marché & Andrei Paskevich (2015):
Let's Verify This with Why3.
International Journal on Software Tools for Technology Transfer (STTT) 17(6),
pp. 709–727,
doi:10.1007/s10009-014-0314-5.
Available at http://hal.inria.fr/hal-00967132/en.
See also http://toccata.lri.fr/gallery/fm2012comp.en.html.
Maria Christakis, K. Rustan M. Leino, Peter Müller & Valentin Wüstholz (2016):
Integrated Environment for Diagnosing Verification Errors.
In: 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16).
Springer,
pp. 424–441,
doi:10.1007/978-3-662-49674-9_25.
David R. Cok (2014):
OpenJML: Software Verification for Java 7 using JML, OpenJDK, and Eclipse.
In: Catherine Dubois, Dimitra Giannakopoulou & Dominique Méry: Proceedings 1st Workshop on Formal Integrated Development Environment,
Electronic Proceedings in Theoretical Computer Science 149,
pp. 79–92,
doi:10.4204/EPTCS.149.8.
Sylvain Dailler, David Hauzar, Claude Marché & Yannick Moy (2018):
Instrumenting a Weakest Precondition Calculus for Counterexample Generation.
Journal of Logical and Algebraic Methods in Programming 99,
pp. 97–113,
doi:10.1016/j.jlamp.2018.05.003.
Available at https://hal.inria.fr/hal-01802488.
Edsger W. Dijkstra (1976):
A discipline of programming.
Series in Automatic Computation.
Prentice Hall Int..
Nikolai Kosmatov, Claude Marché, Yannick Moy & Julien Signoles (2016):
Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014.
In: Tiziana Margaria & Bernhard Steffen: 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA),
Lecture Notes in Computer Science 9952.
Springer,
Corfu, Greece,
pp. 461–478,
doi:10.1007/978-3-319-47166-2_32.
Available at https://hal.inria.fr/hal-01344110.
K. Rustan M. Leino & Valentin Wüstholz (2014):
The Dafny Integrated Development Environment.
In: Catherine Dubois, Dimitra Giannakopoulou & Dominique Méry: Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE 2014, Grenoble, France, April 6, 2014.,
Electronic Proceedings in Theoretical Computer Science 149,
pp. 3–15,
doi:10.4204/EPTCS.149.2.
John W. McCormick & Peter C. Chapin (2015):
Building High Integrity Applications with SPARK.
Cambridge University Press,
doi:10.1017/CBO9781139629294.
Leonardo de Moura & Nikolaj Bjørner (2008):
Z3, An Efficient SMT Solver.
In: TACAS,
Lecture Notes in Computer Science 4963.
Springer,
pp. 337–340,
doi:10.1007/978-3-540-78800-3_24.
Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti & Jacques Julliand (2018):
How testing helps to diagnose proof failures.
Formal Aspects Comput. 30(6),
pp. 629–657,
doi:10.1007/s00165-018-0456-4.
eptcs@eptcs.org