Blog
An Insight Into the AdaCore Ecosystem
Formal Methods Practice and Theory
Claire Dross
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…
Yannick Moy
Rod Chapman on Software Security
Rod Chapman gave an impactful presentation at Bristech conference last year. His subject: programming Satan's computer! His way of pointing out how…
Emma Adby
AdaCore attends FOSDEM
Earlier this month AdaCore attended FOSDEM in Brussels, an event focused on the use of free and open source software. Two members of our technical…
Pat Rogers
Getting started with the Ada Drivers Library device drivers
Yannick Moy
Proving Tetris With SPARK in 15 Minutes
I gave last week a 15-minutes presentation at FOSDEM conference of how you can prove interesting properties of Tetris with SPARK. Here is the…
Raphaël Amiard, Yannick Moy, Pierre-Marie de Rodat
Going After the Low Hanging Bug
At AdaCore, we have a strong expertise in deep static analysis tools (CodePeer and SPARK), and we have been relying on the compiler GNAT and our…
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.