Blog

Yannick Moy

GNATprove Tips and Tricks: Proving the Ghost Common Divisor (GCD)

Euclid's algorithm for computing the greatest common divisor of two numbers is one of the first ones we learn in school, and also one of the first…

Emmanuel Briot

New strings package in GNATCOLL

This post describes the new GNATCOLL.Strings package, and the various optimizations it performs to provide improved performance.

Jerome Guitton, Jérôme Lambourg, Joel Brobecker

Simics helps run 60 000 GNAT Pro tests in 24 hours

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…