Jean-Raymond Abrial & Dominique Cansell (2003):
Click'n Prove: Interactive Proofs within Set Theory.
In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs'03,
Lecture Notes in Computer Science 2758.
Springer,
pp. 1–24,
doi:10.1007/10930755_1.
Wolfgang Ahrendt, Bernhard Beckert, Wolfram Menzel, Wolfgang Reif & Gerhard Schellhorn (1998):
Automated Deduction - A Basis for Applications, chapter Integrating Automated and Interactive Theorem Proving,
Applied Logic Series 9.
Springer, Dordrecht,
doi:10.1007/978-94-017-0437-3.
Stefan Berghofer (2012):
Verification of Dependable Software using SPARK and Isabelle.
In: Jörg Brauer, Marco Roveri & Hendrik Tews: 6th International Workshop on Systems Software Verification,
OpenAccess Series in Informatics (OASIcs) 24,
Dagstuhl, Germany,
pp. 15–31,
doi:10.4230/OASIcs.SSV.2011.15.
Jasmin Christian Blanchette, Sascha Böhme & Lawrence C. Paulson (2013):
Extending Sledgehammer with SMT Solvers.
J. Autom. Reasoning 51(1),
pp. 109–128,
doi:10.1007/978-3-642-22438-6_11.
François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond & Andrei Paskevich (2013):
Preserving User Proofs Across Specification Changes.
In: Ernie Cohen & Andrey Rybalchenko: Verified Software: Theories, Tools, Experiments (5th International Conference VSTTE),
Lecture Notes in Computer Science 8164.
Springer,
Atherton, USA,
pp. 191–201,
doi:10.1007/978-3-642-54108-7_10.
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.
See also http://toccata.lri.fr/gallery/fm2012comp.en.html.
Roderick Chapman & Florian Schanda (2014):
Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK.
In: Gerwin Klein & Ruben Gamboa: Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings,
Lecture Notes in Computer Science 8558.
Springer,
pp. 17–26,
doi:10.1007/978-3-319-08970-6_2.
Jean-Christophe Filliâtre & Andrei Paskevich (2013):
Why3 — Where Programs Meet Provers.
In: Matthias Felleisen & Philippa Gardner: Proceedings of the 22nd European Symposium on Programming,
Lecture Notes in Computer Science 7792.
Springer,
pp. 125–128,
doi:10.1007/978-3-642-37036-6_8.
David Hauzar, Claude Marché & Yannick Moy (2016):
Counterexamples from Proof Failures in SPARK.
In: Rocco De Nicola & Eva Kühn: Software Engineering and Formal Methods,
Lecture Notes in Computer Science,
Vienna, Austria,
pp. 215–233,
doi:10.1007/978-3-319-41591-8_15.
Martin Hentschel, Reiner Hähnle & Richard Bubel (2016):
An Empirical Evaluation of Two User Interfaces of an Interactive Program Verifier.
In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering,
ASE 2016,
pp. 403–413,
doi:10.1007/s10726-011-9236-8.
Martin Hentschel, Reiner Hähnle & Richard Bubel (2016):
The Interactive Verification Debugger: Effective Understanding of Interactive Proof Attempts.
In: Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering,
ASE 2016.
ACM,
pp. 846–851,
doi:10.1145/2970276.2970292.
John W. McCormick & Peter C. Chapin (2015):
Building High Integrity Applications with SPARK.
Cambridge University Press,
doi:10.1017/CBO9781139629294.
Farhad Mehta (2007):
Supporting Proof in a Reactive Development Environment.
In: Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods,
SEFM'07.
IEEE Computer Society,
pp. 103–112,
doi:10.1109/SEFM.2007.40.
Guillaume Melquiond & Raphaël Rieu-Helft (2018):
A Why3 Framework for Reflection Proofs and its Application to GMP's Algorithms.
In: 9th International Joint Conference on Automated Reasoning,
Oxford, United Kingdom,
doi:10.1007/978-3-319-94205-6_13.
Available at https://hal.inria.fr/hal-01699754.
Guillaume Petiot, Nikolai Kosmatov, Bernard Botella, Alain Giorgetti & Jacques Julliand (2016):
Your Proof Fails? Testing Helps to Find the Reason.
In: Tests and Proofs - 10th International Conference,
Lecture Notes in Computer Science 9762.
Springer,
pp. 130–150,
doi:10.1007/978-3-319-41135-4_8.
eptcs@eptcs.org