@inproceedings(barrett11cade,
 author       = {Clark Barrett and Christopher L. Conway and Morgan Deters and Liana Hadarean and Dejan Jovanovi\'{c} and Tim King and Andrew Reynolds and Cesare Tinelli},
 year         = {2011},
 title        = {{CVC4}},
 booktitle    = {Computer Aided Verification},
 series       = {Lecture Notes in Computer Science},
 volume       = {6806},
 publisher    = {Springer},
 pages        = {171--177},
 doi          = {10.1007/978-3-642-22110-1_14},
)
@techreport(becker21rr,
 author       = {Benedikt Becker and Belo Louren\c{c}o, Cl{\'a}udio and Claude March{\'e}},
 year         = {2021},
 title        = {Giant-step Semantics for the Categorisation of Counterexamples},
 type         = {Research Report},
 number       = {RR-9407},
 institution  = {Inria},
 url          = {https://hal.inria.fr/hal-03213438},
)
@misc(alt-ergo,
 author       = {Fran\c{c}ois Bobot and Sylvain Conchon and \'Evelyne Contejean and Mohamed Iguernelala and St\'ephane Lescuyer and Alain Mebsout},
 year         = {2008},
 title        = {The {Alt-Ergo} Automated Theorem Prover},
 note         = {\url{http://alt-ergo.lri.fr/}},
)
@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},
 url          = {http://hal.inria.fr/hal-00967132/en},
 note         = {See also \url{http://toccata.lri.fr/gallery/fm2012comp.en.html}},
)
@inproceedings(christakis16tacas,
 author       = {Maria Christakis and K. Rustan M. Leino and Peter M{\"u}ller and Valentin W{\"u}stholz},
 year         = {2016},
 title        = {Integrated Environment for Diagnosing Verification Errors},
 booktitle    = {22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16)},
 publisher    = {Springer},
 pages        = {424--441},
 doi          = {10.1007/978-3-662-49674-9_25},
)
@inproceedings(cok14,
 author       = {David R. Cok},
 year         = {2014},
 title        = {{OpenJML}: Software Verification for {Java 7} using {JML}, {OpenJDK}, and {Eclipse}},
 editor       = {Catherine Dubois and Dimitra Giannakopoulou and Dominique M{\'{e}}ry},
 booktitle    = {Proceedings 1st Workshop on Formal Integrated Development Environment},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {149},
 pages        = {79--92},
 doi          = {10.4204/EPTCS.149.8},
)
@article(dailler18jlamp,
 author       = {Sylvain Dailler and David Hauzar and Claude March{\'e} and Yannick Moy},
 year         = {2018},
 title        = {Instrumenting a Weakest Precondition Calculus for Counterexample Generation},
 journal      = {Journal of Logical and Algebraic Methods in Programming},
 volume       = {99},
 pages        = {97--113},
 doi          = {10.1016/j.jlamp.2018.05.003},
 url          = {https://hal.inria.fr/hal-01802488},
)
@book(Dijkstra76,
 author       = {Edsger W. Dijkstra},
 year         = {1976},
 title        = {A discipline of programming},
 series       = {Series in Automatic Computation},
 publisher    = {Prentice Hall Int.},
)
@inproceedings(kosmatov16isola,
 author       = {Nikolai Kosmatov and Claude March{\'e} and Yannick Moy and Julien Signoles},
 year         = {2016},
 title        = {Static versus Dynamic Verification in {Why3}, {Frama-C} and {SPARK 2014}},
 editor       = {Tiziana Margaria and Bernhard Steffen},
 booktitle    = {7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA)},
 series       = {Lecture Notes in Computer Science},
 volume       = {9952},
 publisher    = {Springer},
 address      = {Corfu, Greece},
 pages        = {461--478},
 doi          = {10.1007/978-3-319-47166-2_32},
 url          = {https://hal.inria.fr/hal-01344110},
)
@inproceedings(leino14fide,
 author       = {K. Rustan M. Leino and Valentin W{\"{u}}stholz},
 year         = {2014},
 title        = {The {Dafny} Integrated Development Environment},
 editor       = {Catherine Dubois and Dimitra Giannakopoulou and Dominique M{\'{e}}ry},
 booktitle    = {Proceedings 1st Workshop on Formal Integrated Development Environment, {F-IDE} 2014, Grenoble, France, April 6, 2014.},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {149},
 pages        = {3--15},
 doi          = {10.4204/EPTCS.149.2},
)
@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(demoura08tacas,
 author       = {Leonardo de Moura and Bj{\o}rner, Nikolaj},
 year         = {2008},
 title        = {{Z3}, An Efficient {SMT} Solver},
 booktitle    = {TACAS},
 series       = {Lecture Notes in Computer Science},
 volume       = {4963},
 publisher    = {Springer},
 pages        = {337--340},
 doi          = {10.1007/978-3-540-78800-3_24},
)
@article(petiot18fac,
 author       = {Guillaume Petiot and Nikolai Kosmatov and Bernard Botella and Alain Giorgetti and Jacques Julliand},
 year         = {2018},
 title        = {How testing helps to diagnose proof failures},
 journal      = {Formal Aspects Comput.},
 volume       = {30},
 number       = {6},
 pages        = {629--657},
 doi          = {10.1007/s00165-018-0456-4},
)