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.
Information Hiding and Context Management in SPARK
A previous blog explored the verification of the formal hashed sets package in SPARKlib. This post will explain the techniques used to simplify the…
Reasoning about Linked Structures in an Array
Reasoning about linked data structures within an array is complicated, requiring high-level concepts such as reachability and inductive reasoning.…
Formally Verified Hashed Sets in Ada SPARK
This blog explores the formal verification of an implementation of bounded hashed sets in Ada SPARK.
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…
Handling Aliasing through Pointers in SPARK
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…
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…
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…
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…
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…
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…
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.…