Blog

Johannes Kanig

Hash it and Cache it

A new feature of SPARK2014 allows to use a memcached server to share proof results between runs of the SPARK tools and even between developers on…

Raphaël Amiard, Pierre-Marie de Rodat

Introducing Libadalang

AdaCore is working on a host of tools that works on Ada code. The compiler, GNAT, is the most famous and prominent one, but it is far from being the…

Yannick Moy

New Year's Resolution for 2017: Use SPARK, Say Goodbye to Bugs

​NIST has recently published a report called "Dramatically Reducing Software Vulnerabilities"​ in which they single out five approaches which have…

Johannes Kanig

SPARK and CodePeer, a Good Match!

It turns out that the CodePeer engine can be used as a powerful prover for SPARK programs. This feature will be available in the next version of…

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