Content by 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.
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…
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…
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…
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…
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…
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…
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…
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…
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…