The AdaCore Blog

Yannick Moy

GNATprove Tips and Tricks: Keeping Justifications Up-To-Date

GNATprove supports the suppression of warnings and justification of check messages with pragmas inserted in the source code. But these justifications…

Lena Comar

ProofInUse is coming!

Yannick Moy

SPARK 2014 Rationale: Functional Update

While attribute Old allows expressing inside postconditions the value of objects at subprogram entry, this is in general not enough to conveniently…

Emma Adby

A Busy Schedule Ahead!

Yannick Moy

SPARK 2014 Rationale: Object Oriented Programming

Object Oriented Programming is known for making it particularly difficult to analyze programs, because the subprograms called are not always known…

Introducing the AdaCore Blog

We’re pleased to announce the launch of the AdaCore Blog providing an insight into the AdaCore Ecosystem.

Tristan Gingold, Yannick Moy

Tetris in SPARK on ARM Cortex M4

Cyrille Comar

Welcome To AdaCore's Blog

I'm proud, if not a bit nervous, to be the one firing the very first post on this brand new blog. Why are we starting a corporate blog at this time?…

Yannick Moy

SPARK 2014 Rationale: Ghost Code

A common situation when proving properties about a program is that you end up writing additional code whose only purpose is to help proving the…

Yannick Moy

Using Coq to Verify SPARK 2014 Code

In the first release of SPARK 2014, GNATprove only provided support for automatic provers, in particular Alt-Ergo. Automatic provers are very handy…

Johannes Kanig

SPARK 15: Errors, Warnings and Checks

The messages issued by the SPARK toolset will change a bit in the next version of both SPARK Pro and SPARK GPL. This post explains the change and the…

Yannick Moy

Using SPARK to Prove AoRTE in Robot Navigation Software

Correctness of robot software is a challenge. Just proving the absence of run-time errors (AoRTE) in robot software is a challenge big enough that…