Programming in Ada 2012, 2014. ,
DOI : 10.1017/CBO9781139696616
The SMT-LIB Standard: Version 2.0, 2010. ,
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder, Interactive Theorem Proving, pp.131-146, 2010. ,
DOI : 10.1007/978-3-642-14052-5_11
The Alt- Ergo automated theorem prover, 2008. ,
Why3: Shepherd your herd of provers, Int. Workshop on Intermediate Verification Languages, pp.53-64, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00790310
Let???s verify this with Why3, International Journal on Software Tools for Technology Transfer, vol.7, issue.5, pp.709-727, 2015. ,
DOI : 10.1007/s10009-014-0314-5
Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK, Interactive Theorem Proving, pp.17-26, 2014. ,
DOI : 10.1007/978-3-319-08970-6_2
Integrated Environment for Diagnosing Verification Errors, 2016. ,
DOI : 10.1007/978-3-662-49674-9_25
VCC: A Practical System for Verifying Concurrent C, Theorem Proving in Higher Order Logics, 2009. ,
DOI : 10.1007/978-3-540-74591-4_15
Improved usability and performance of SMT solvers for debugging specifications, International Journal on Software Tools for Technology Transfer, vol.45, issue.3, pp.467-481, 2010. ,
DOI : 10.1007/s10009-010-0138-x
OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse, Electronic Proceedings in Theoretical Computer Science, vol.149, pp.79-92, 2014. ,
DOI : 10.4204/EPTCS.149.8
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, Computer Aided Verification, pp.173-177, 2007. ,
DOI : 10.1007/978-3-540-73368-3_21
Why3 ??? Where Programs Meet Provers, European Symposium on Programming, pp.125-128, 2013. ,
DOI : 10.1007/978-3-642-37036-6_8
Understanding Counterexamples with explain, Computer Aided Verification, pp.453-456, 2004. ,
DOI : 10.1007/978-3-540-27813-9_35
Counterexamples from proof failures in the SPARK program verifier, Research Report Inria, vol.8854, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01271174
VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java, NASA Formal Methods, pp.41-55, 2011. ,
DOI : 10.1007/11691372_19
The Boogie Verification Debugger, Software Engineering and Formal Methods, pp.407-414, 2011. ,
Generating error traces from verification-condition counterexamples, Science of Computer Programming, vol.55, issue.1-3, pp.1-3, 2005. ,
DOI : 10.1016/j.scico.2004.05.016
The Dafny Integrated Development Environment, Electronic Proceedings in Theoretical Computer Science, vol.149, pp.3-15, 2014. ,
DOI : 10.4204/EPTCS.149.2
Building High Integrity Applications with SPARK, 2015. ,
DOI : 10.1017/CBO9781139629294
Z3: An Efficient SMT Solver, LNCS, vol.4963, pp.337-340, 2008. ,
DOI : 10.1007/978-3-540-78800-3_24
Using Debuggers to Understand Failed Verification Attempts, Formal Methods, pp.73-87, 2011. ,
DOI : 10.1145/249094.249108
Your Proof Fails? Testing Helps to Find the Reason, 2015. ,
DOI : 10.1007/978-3-662-49674-9_25
Using Answer Set Programming in the Development of Verified Software, Technical Communications of the 28th Int. Conf. on Logic Programming. LIPIcs, pp.72-85, 2012. ,
Kodkod: A Relational Model Finder, pp.632-647, 2007. ,
DOI : 10.1007/978-3-540-71209-1_49