Tutorials
- The Why verification tool Tutorial and Reference Manual
- ACSL by Example
- Jessie Plugin for Frama-C Tutorial
- Tokeneer Discovery: A Spark Tutorial
- Proof of Absence of Run-Time Error in SPARK Tutorial
Papers and Articles
- Formal Verification of Aerospace Software
- The Convergence of Compiler Technology and Program Verification
- Maximal and Compositional Pattern-Based Loop Invariants
- Integrating Formal Program Verification with Testing
- Why Hi-Lite Ada?
- Hi-Lite - Verification by Contract
- Correct Code Containing Containers
- A Pragmatic View of Formal Methods: the Hi-Lite Project
- Examples of Possible Industrial Use of Hi-Lite
- FLOSS, COTS, and Safety: A Business Perspective
- A (Very) Short Introduction to SPARK: Language, Toolset, Projects, Formal Methods & Certication
- Expressive vs. Permissive Languages: Is that the question?
- Tokeneer: Beyond Formal Program Verification
- Algebraic Types and Pattern Matching in Why
- Frama-C Publications
Books
- Ada 2005 Rationale: Introduction
- Ada 2005 Rationale: Object oriented model
- Ada 2005 Rationale: Access types
- Ada 2005 Rationale: Structure and visibility
- Ada 2005 Rationale: Tasking and Real-Time
- Ada 2005 Rationale: Exceptions, generics etc
- Ada 2005 Rationale: Predefined library
- Ada 2005 Rationale: Containers
- Ada 2005 Rationale: Epilogue
- First chapter of the SPARK Book by John Barnes
Presentations
- Formal Verification of Aerospace Software presented at DASIA 2013 conference
- Combining Formal Program Verification and Testing presented at the Embedded World 2013 conference
- Combining Formal Program Verification and Testing presented at the FOSDEM 2013 conference
- Integration of tests and proofs presented at the ERTS2 2012 conference
- Hi-Lite presented at the 2nd Workshop on Theorem Proving in Certification
- Hi-Lite presented at Safety-critical Systems Symposium 2011
- Formal verification and Hi-Lite presented at Fraunhofer FIRST
- Hi-Lite presented at IRILL
- Hi-Lite Kickoff (in French)
- SMT provers: an introduction
- Why — An intermediate language for deductive program verification
- Software Analysis Tools at AdaCore
- Hi-Lite in one slide
- SPARK in one slide
- Tokeneer: Beyond Formal Program Verification
Videos
- Hi-Lite and Open Source presented at IRILL Days 2010
- Introducing Project Hi-Lite
- Demo on using Frama-C with the Jessie plugin
- Introducing SPARK Pro Webinar
- Getting started with SPARK Webinar
- Introducing SPARK 9.0 Webinar
- Introducing CodePeer Webinar
- CodePeer by Example: Find-the-bug Challenge 1
- CodePeer by Example: Find-the-bug Challenge 2
- CodePeer by Example: Find-the-bug Challenge 3
- CodePeer by Example: Find-the-bug Challenge 4
- CodePeer by Example: Find-the-bug Challenge 5