Blog

Yannick Moy

SPARK Cheat Sheets (en & jp)

The SPARK cheat sheet usually distributed in trainings has recently been translated to Japanese. Here they are, both in English and in Japanese. My…

Fabien Chouteau

Make with Ada: DIY instant camera

There are moments in life where you find yourself with an AdaFruit thermal printer in one hand, and an OpenMV camera in the other.

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…