SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Certification

The Eight Reasons For Using SPARK

by Yannick Moy in Formal Verification, Design Method, Certification, Papers and Slides – September 21, 2015

Based on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most commonly targeted when using SPARK. Most projects only target a few of them, but in theory one could try to achieve all of them with SPARK on a project. This list may be useful for those who want to assess if the SPARK technology can be of benefit in their context, and to existing SPARK users to compare their existing practice with what others do.

Use of SPARK in a Certification Context

by Yannick Moy in Formal Verification, Certification, News, Papers and Slides – April 30, 2014

Using SPARK or any other formal method in a certification requires that the applicant agrees with the certification authority on the verification objectives that this use of formal methods allows to reach, and how this is obtained and documented. In order to facilitate this process, the participants to the workshop on Theorem Proving in Certification have produced a draft set of guidelines, now publicly available.

Case Study for System to Software Integrity Includes SPARK 2014

by Yannick Moy in Formal Verification, Certification, News, Papers and Slides – January 21, 2014

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.

Muen Separation Kernel Written in SPARK

by Yannick Moy in Language, Formal Verification, Certification, Open Source, News – December 19, 2013

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.

not Taking Assumptions for Granted

by Yannick Moy in Language, Certification – February 14, 2013

The Merriam-Webster dictionnary defines an assumption as “a fact or statement (as a proposition, axiom, postulate, or notion) taken for granted”. This is indeed the role that assumptions play in formal verification of programs, as performed in Frama-C platform or GNATprove.

Prove & Fly!

by Yannick Moy in Certification, Events – December 14, 2011

On December 5-6, I participated in the 2nd workshop on Theorem Proving in Certification, in Cambridge (UK). This turned out to be even more interesting than last year’s program promised.