| Verification of Programs with Pointers in SPARK. | 0 | 0.34 | 2020 |
| Tutorial: A Practical Introduction to Formal Development and Verification of High-Assurance Software with SPARK | 0 | 0.34 | 2019 |
| Safe Dynamic Memory Management In Ada And Spark | 0 | 0.34 | 2018 |
| Lightweight Interactive Proving inside an Automatic Program Verifier. | 1 | 0.35 | 2018 |
| Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software. | 0 | 0.34 | 2018 |
| Instrumenting a weakest precondition calculus for counterexample generation. | 1 | 0.35 | 2018 |
| Auto-Active Proof of Red-Black Trees in SPARK. | 2 | 0.41 | 2017 |
| Focused Certification of an Industrial Compilation and Static Verification Toolchain. | 0 | 0.34 | 2017 |
| Automating The Verification Of Floating-Point Programs | 0 | 0.34 | 2017 |
| High-Integrity Multitasking in SPARK: Static Detection of Data Races and Locking Cycles | 1 | 0.35 | 2016 |
| Counterexamples from Proof Failures in SPARK. | 4 | 0.41 | 2016 |
| Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. | 4 | 0.44 | 2016 |
| Spark 2014 And Gnatprove A Competition Report From Builders Of An Industrial-Strength Verifying Compiler | 0 | 0.34 | 2015 |
| Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification. | 3 | 0.50 | 2014 |
| Testing or Formal Verification: DO-178C Alternatives and Industrial Experience | 18 | 0.83 | 2013 |
| Source code as the key artifact in requirement-based development: the case of ada 2012 | 1 | 0.37 | 2012 |
| Maximal and Compositional Pattern-Based Loop Invariants. | 2 | 0.35 | 2012 |
| Integration von Formaler Verifikation und Test. | 0 | 0.34 | 2012 |
| Hi-Lite - Verification by Contract. | 1 | 0.35 | 2011 |
| Correct code containing containers | 6 | 0.49 | 2011 |
| Modular inference of subprogram contracts for safety checking | 10 | 0.53 | 2010 |
| Sufficient preconditions for modular assertion checking | 15 | 0.79 | 2008 |
