AdaCore Blog

Claire Dross

Claire Dross has a PhD in deductive verification of programs using a satisfiability modulo theory solver with the Universite Paris-Sud. She also has an engineering degree from the Ecole Polytechnique and an engineering degree from the Ecole Nationale Superieure des Telecommunications. At AdaCore, she works full-time on the formal verification SPARK 2014 toolset.

12 entries written by Claire Dross

by Claire Dross

Research Corner - Auto-active Verification in SPARK

GNATprove performs auto-active verification, that is, verification is done automatically, but usually requires annotations by the user to succeed. In SPARK, annotations are most often given in the form of contracts (pre and postconditions). But some language features, in particular ghost code, allow proof guidance to be much more involved. In a paper we are presenting at NASA Formal Methods symposium 2017, we describe how an imperative red black tree implementation in SPARK was verified using intensive auto-active verification.

#Formal Verification    #SPARK   

by Claire Dross

Automatic Generation of Frame Conditions for Array Components

One of the most important challenges for SPARK users is to come up with adequate contracts and annotations, allowing GNATprove to verify the expected properties in a modular way. Among the annotations mandated by the SPARK toolset, the hardest to come up with are probably loop invariants. A previous post explains how GNATprove can automatically infer loop invariants for preservation of unmodified record components, and so, even if the record is itself nested inside a record or an array. Recently, this generation was improved to also support the simplest cases of partial array updates. We describe in this post in which cases GNATprove can, or cannot, infer loop invariants for preservation of unmodified array components.

#Formal Verification    #SPARK   

by Claire Dross

SPARK 2014 Rationale: Support for Type Invariants

Type invariants are used to model properties that should always hold for users of a data type but can be broken inside the data type implementation. Type invariant are part of Ada 2012 but were not supported in SPARK until SPARK Pro 17.

#SPARK   

by Claire Dross

Automatic Generation of Frame Conditions for Record Components

Formal verification tools like GNATprove rely on the user to provide loop invariants to describe the actions performed inside loops. Though the preservation of variables which are not modified in the loop need not be mentioned in the invariant, it is in general necessary to state explicitly the preservation of unmodified object parts, such as record fields or array elements. These preservation properties form the loop’s frame condition. As it may seem obvious to the user, the frame condition is unfortunately often forgotten when writing a loop invariant, leading to unprovable checks. To alleviate this problem, the GNATprove tool now generates automatically frame conditions for preserved record components. In this post, we describe this new feature on an example.

#Formal Verification    #SPARK   

by Claire Dross

Quantifying over Elements of a Container

Containers holding several items of the same type such as arrays, lists, or sets are a common occurrence in computer programs. Stating a property over such containers often involves quantifying over the elements they contain. The way quantified formulas over containers are translated for proof can be tuned in GNATprove using a specific annotation.

#Formal Verification    #SPARK   

by Claire Dross

A quick glimpse at the translation of Ada integer types in GNATprove

In SPARK, as in most programming languages, there are a bunch of bounded integer types. On the other hand, Why3 only has mathematical integers and a library for bitvectors. Since bitwise operations can only be done on modular types in Ada, we currently translate arithmetic operations on signed integer types as operations on mathematical integers and arithmetic operations on modular types as operation on bitvectors. The only remaining question now is, how do we encode specific bounds of the Ada types into our Why3 translation ? In this post, I will present three different ways we tried to do this and explain which one we currently use and why.

#Formal Verification    #SPARK   

by Claire Dross

External Axiomatizations: a Trip Into SPARK’s Internals

There are cases expressing all the specification of a package in SPARK is either impossible (for example if you need to link them to elements of the mathematical world, like trigonometry functions), cumbersome (especially if they require concepts that cannot easily be described using contracts, like transitivity, counting, summation...), or simply inefficient, for big and complex data structures like containers for example. In these cases, a user can provide directly a manually written Why3 translation for an Ada package using a feature named external axiomatizations. Coming up with this manual translation requires both a knowledge of the WhyML language and a minimal understanding of GNATprove's mechanisms and is therefore reserved to advanced users.

#Formal Verification    #SPARK   

by Claire Dross

Manual Proof with Ghost Code in SPARK 2014

Guiding automatic solvers by adding intermediate assertions is a commonly used technique. We can go further in this direction, by adding complete pieces of code doing nothing, generally called ghost code, to guide the automated reasoning. This is an advanced feature, for people willing to manually guide proofs. Still, it is all in SPARK 2014 and thus does not require the user to learn a new language. We explain here how we can achieve inductive proofs on a permutation function.

#Formal Verification    #SPARK   

by Claire Dross

Contracts of Functions in SPARK 2014

In SPARK 2014, we can write a function F and annotate it with a pre and a postcondition. In this post, we explain how the SPARK 2014 proof tool handles a call to such a function.

#Formal Verification    #SPARK   

by Claire Dross

SPARK 2014 Rationale: Verifying Properties over Formal Containers

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.

#Language    #Formal Verification    #SPARK   

by Claire Dross

SPARK 2014 Rationale: Expressing Properties over Formal Containers

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.

#Language    #Formal Verification    #SPARK   

by Claire Dross

SPARK 2014 Rationale: Formal Containers

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.

#Language    #Formal Verification    #SPARK