Modernizing Adacore's Open-Source Involvement

Through the adoption of GitHub we have taken our first step on the way to having a more collaborative and dynamic interaction with, both our users and open source technologies.

SPARK 16: Generating Counterexamples for Failed Proofs

While the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would automatically find values of variables showing why a proof fails. SPARK Pro 16, to be released in 2016, is going to introduce such a feature. If a proof fails, it attempts to generate a counterexample exhibiting the problem. This post introduces this new feature, developed in the scope of the ProofInUse laboratory.

ARM TechCon and NBAA Conference 2015

We are continuing to develop tools for use within projects that require reliable and secure embedded software for ARM. Our engineering team have been busy creating demos running on ARM technology, such as Tetris in SPARK on ARM Cortex M4.

GNATprove Tips and Tricks: User Profiles

One of the most difficult tasks when using proof techniques is to interact with provers, in particular to progressively increase proof power until everything that should be proved is proved. Until the last release, increasing the proof power meant operating on three separate switches. There is now a simpler solution based on a new switch --level, together with a simpler proof panel in GPS for new users.

Using reference types to handle persistent objects

The Ada 2012 standard introduced user-defined references. The main idea behind this is simplifying the access to elements in a container. But you can use them to control the life-circle of your persistent objects. Let's see how it could work.

HIS Conference 2015, Bristol

We are excited to be sponsoring and exhibiting at the 2nd annual High Integrity Software conference, taking place on 5th November 2015 at The Royal Marriott Hotel in Bristol.

AdaCore Tech Days 2015

SPARK 2014 Rationale: Variables That Are Constant

The SPARK tools now support yet another feature that allows users to better specify the intended behavior of their programs. This new feature enables users to declare that specific variables can only be updated during the elaboration of their enclosing package. Read on if you want to know more...

The Eight Reasons For Using SPARK

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.

Traits-Based Containers

This post describes the design of a new containers library. It highlights some of the limitations of the standard Ada containers, and proposes a new approach using generic packages as formal parameters to make these new containers highly configurable at compile time.

New Book About SPARK 2014

I am very pleased to announce that a book is now available for those who want to learn formal verification with SPARK 2014. This book was written by Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College. We've been interacting a lot with them since they started in 2013, and the result of these interactions is quite satisfying!

Make with Ada : From bits to music

I started out as an electronic musician, so one of my original motivations when I learnt programming was so that I could eventually *program* the sounds I wanted rather than just use already existing software to do it.

2015: A Space Ada‑ssey

AdaCore has a long history of providing tools and support to develop mission critical applications for Space. Check out this video we made and showed at the conference to see which ones!

SPARK 2014 Rationale: Type Predicates

Preconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar properties for the program's data? It turns out Ada 2012 defined such a construct, type predicates, which was not supported in SPARK until now. And now it is.

Make with Ada: "The Eagle has landed"

July 20, 1969, 8:18 p.m. UTC, while a bunch of guys were about to turn blue on Earth, commander Neil A. Armstrong confirms the landing of his Lunar Module (LM), code name Eagle, on the moon. Will you be able to manually land Eagle on the Sea of Tranquillity?

Farewell Robert...

It is with great sadness that I have to announce the death of Robert Dewar...

Make with Ada: All that is useless is essential

A few weeks ago I discovered the wonderful world of solenoid engines. The idea is simple: take a piston engine and replace explosion with electromagnetic field. In this article I will experiment a solenoid engine using a hacked hard drive and a software controller on a STM32F4 .

SPARKSkein: From tour-de-force to run-of-the-mill Formal Verification

In 2010, Rod Chapman released an implementation in SPARK of the Skein cryptographic hash algorithm, and he proved that this implementation was free of run-time errors. That was a substantial effort with the previous version of the SPARK technology. We have recently translated the code of SPARKSkein from SPARK 2005 to SPARK 2014, and used GNATprove to prove absence of run-time errors in the translated program. The difference between the two technologies is striking. The heroic effort that Rod put in the formal verification of the initial version of SPARKSkein could now be duplicated with modest effort and modest knowledge of the technology, thanks to the much greater proof automation that the SPARK 2014 technology provides, as well as various features that lower the need to provide supporting specifications, most notably contracts on internal subprograms and loop invariants.

How to prevent drone crashes using SPARK

The Crazyflie is a very small quadcopter sold as an open source development platform: both electronic schematics and source code are directly available on their GitHub and its architecture is very flexible. Even if the Crazyflie flies out of the box, it has not been developed with safety in mind: in case of crash, its size, its weight and its plastic propellers won’t hurt anyone! But what if the propellers were made of carbon fiber, and shaped like razor blades to increase the drone’s performance? In theses circumstances, a bug in the flight control system could lead to dramatic events. In this post, I present the work I did to rewrite the stabilization system of the Crazyflie in SPARK 2014, and to prove that it is free of runtime errors. SPARK also helped me to discover little bugs in the original firmware, one of which directly related with overflows. Besides the Crazyflie, this work could be an inspiration for others to do the same work on larger and more safety-critical drones.

How Our Compiler Learnt From Our Analyzers

Program analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent with the way that the compiler interprets it to generate an executable, or the information computed is irrelevant, possibly misleading. For example, if the analyzer says that there are no possible run-time errors in a program, and you rely on this information to compile with dynamic checking off, it is crucial that no run-time error could occur as a result of a divergence of opinion between the analyzer and the compiler on the meaning of an instruction. We recently discovered such an inconsistency in how our compiler and analyzers dealt with floating-point exponentiation, which lead to a change in how GNAT now compile these operations.