News
- French open-source project aims to meet DO-178C [Embedded news]
- Formal verification ticks Ada and C for DO-178C [Electronics Weekly]
- Hi-Lite project to promote formal methods for high integrity software [Embedded Control Europe]
- Le projet Hi-Lite veut imposer la validation formelle pour les sytèmes critiques [Clubic]
- Applications critiques embarquées : chercheurs et industriels s’associent autour du projet Hi-Lite [Mesures]
- Un consortium autour des méthodes formelles pour les logiciels fortement intégrés [Industries et Technologies]
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
- 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 & Certi cation
- 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
- 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
- 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