AdaCore Blog

Claire Dross

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.

17 entries written by Claire Dross

by Claire Dross

SPARK, Beyond Normal Termination

When teaching SPARK to my students, I generally explain the central position of contracts in formal verification in the following way: Contracts of subprograms summarize their behavior - preconditions constrain their inputs, while postconditions describe their effects. It is an easy way to see contracts, However, not returning normally, for example looping forever or raising exceptions, is definitely a significant effect of a subprogram. Modeling that effect would be beneficial because if it occurs in an unexpected way it might cause the entire program to derail. Release 24.0 of SPARK includes contracts that can be used to reason about subprograms which do not return normally. This blog post describes them.

by Claire Dross

Handling Aliasing through Pointers in SPARK

As I explained in a blog post a couple of years ago, pointers are subjected to a strict ownership policy in SPARK. It prevents aliasing and allows for an efficient formal verification model. Of course, it comes at the cost of restrictions which might not be applicable to all usage. In particular, while ownership makes it possible to represent certain recursive data-structures, those involving cycles or sharing are de-facto forbidden. This is a choice, and not every proof tool did the same. For example, the WP plug-in of Frama-C supports pointers with arbitrary aliasing. If some information about the separation of memory cells is necessary to verify a program, then the user shall give the annotation explicitly. I have investigated modeling pointers with aliasing in SPARK as indices in a big memory array. I will present the results of my experiments in this blog post. We will see that, while such a representation is indeed possible modulo some hiding in SPARK, it can quickly become rather heavy in practice.

#SPARK #Data Structures #Formal Verification

by Claire Dross

Relaxing the Data Initialization Policy of SPARK

SPARK always being under development, new language features make it in every release of the tool, be they previously unsupported Ada features (like access types) or SPARK specific developments. However, new features generally take a while to make it into actual user code. The feature I am going to present here is in my experience an exception, as it was used both internally and by external users before it made it into any actual release. It was designed to enhance the verification of data initialization, whose limitations have been a long standing issue in SPARK.

#Formal Verification #SPARK

by Claire Dross

Pointer Based Data-Structures in SPARK

As seen in a previous post, it is possible to use pointers (or access types) in SPARK provided the program abides by a strict memory ownership policy designed to prevent aliasing. We will show in this post how to define pointer-based data-structures in SPARK and how to traverse them without breaking the ownership policy.

#SPARK #Formal Verification

by Claire Dross

Using Pointers in SPARK

In this blog post, I will present one of the most interesting additions to the community 2019 version of SPARK: pointer support. One of the core assumption in SPARK has always been the absence of aliasing, so adding pointers without breaking this assumption was quite a challenge. I will explain how this was achieved using an ownership model for pointers (like is done in Rust) through small examples.

#VerificationTools

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.

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