Blog

Yannick Moy

Two Projects to Compute Stats on Analysis Results

Two projects by Daniel King and Martin Becker facilitate the analysis of GNATprove results by exporting the results (either from the log or from the…

Pierre-Marie de Rodat

GNATcoverage moves to GitHub

Jorge Real

Writing on Air

Fabien Chouteau, Arnaud Charlet, Yannick Moy

SPARK Tetris on the Arduboy

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…