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