Blog

Emma Adby

Building High-Assurance Software without Breaking the Bank

Emma Adby

Make With Ada Winners Announced!

Sylvain Dailler

GNATprove Tips and Tricks: a Lemma for Sorted Arrays

We report on the creation of the first lemma of a new lemma library on arrays: a lemma on transitivity of the order in arrays.

Emmanuel Briot

Integrate new tools in GPS (2)

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…

Yannick Moy

GNATprove Tips and Tricks: What’s Provable for Real Now?

One year ago, we presented on this blog what was provable about fixed-point and floating-point computations (the two forms of real types in SPARK).…

Emmanuel Briot

Integrate new tools in GPS

This blog, the first in a series, explains the basic mechanisms that GPS (the GNAT Programming Studio) provides to integrate external tools. A small…

Pat Rogers

Driving a 3D Lunar Lander Model with ARM and Ada

Yannick Moy

Research Corner - SPARK on Lunar IceCube Micro Satellite

Researchers Carl Brandon and Peter Chapin recently presented during conference HILT 2016 their ongoing work to build a micro satellite called Lunar…

Piotr Trojanek

Verifying Tasking in Extended, Relaxed Style

Tasking was one of the big features introduced in the previous release of SPARK 2014. However, GNATprove only supported tasking-related constructs…

Olivier Ramonat

Simplifying our product versioning

Looking at the list of product versions that were expected for 2017 it became clear that we had to review the way we were handling product versioning.

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