Having already presented in previous posts why loop invariants are necessary for formal verification of programs with loops, and what loop invariants are necessary for various loops, we detail here a methodology for how users can come up with the right loop invariants for their loops. This methodology in four steps allows users to progressively add the necessary information in their loop invariants, with the tool GNATprove providing the required feedback at each step on whether the information provided is sufficient or not.
My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study showing how formal verification with SPARK can be included in a larger process to show preservation of properties from the system level down to the software level. The case study is based on the Nose Gear challenge from the Workshop on Theorem Proving in Certification.
We saw in a previous post how we could express complex properties over formal containers using quantified expressions. In this post, I present how these properties can be verified by the proof tool called GNATprove.
The upcoming releases SPARK Pro 14 and SPARK GPL 2014 will be based on the Why3 technology developed by the French research laboratory INRIA. It took us four years, as part of project Hi-Lite, to switch from the older technology to this new one. We are now planning for a closer relationship with INRIA to further evolve this technology, through a common research laboratory that will start operating in October 2014.
The University of Applied Sciences Rapperswil in Switzerland has released last week an open-source separation kernel written in SPARK, which has been proved free from run-time errors. This project is part of the secure multilevel workstation project by Secunet, a German security company, which is using SPARK and Isabelle to create the next generation of secure workstations providing different levels of security to government employees and military personnel. I present why I think this project is worth following closely.
We saw in a previous post how formal containers can be used in SPARK code. In this post, I describe how to express properties over the content of these containers, using quantified expressions.
Zhi Zhang, currently on PhD in Kansas State University, started to formalize SPARK 2014 language in Coq during an internship last summer between CNAM and AdaCore. This work was presented at the HILT Conference last month.
We will present three case studies using SPARK 2014 at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February 2014, in three different domains: rail, space and security. The lessons learned in those three case studies are particularly interesting. Here is the companion paper that we wrote.
SPARK 2014 excludes data structures based on pointers. Instead, one can use the library of formal containers. They are variant of the Ada 2012 bounded containers, specifically designed and annotated to facilitate the proof of programs using them.
In a previous post about pre-call values, I described how the Ada language rules implemented in the compiler prevent surprises when referring to input values in the postcondition, using the Old attribute. Unfortunately, these rules also make it difficult to express some complex postconditions that may be useful when doing formal verification. In this post, I describe how contract cases allow the expression of these complex contracts, while still detecting potential problems with uses of the Old attribute.