Blog Posts 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.
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…
Claire Dross
Handling Aliasing through Pointers in SPARK
Yannick Moy, Claire Dross
Proving the Correctness of GNAT Light Runtime Library
The GNAT light runtime library is a version of the runtime library targeted at embedded platforms and certification, which has been certified for use…
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…
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…
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…
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…
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…
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.…
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…
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…
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…