Blog
An Insight Into the AdaCore Ecosystem
Proving Safety at Scale: SPARK, RISC-V, and NVIDIA’s Security Strategy
Read More
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).…
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