Blog
An Insight Into the AdaCore Ecosystem
Formally Verified Hashed Sets in Ada SPARK
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…
Gem #161 : So long and thanks for all the memories!
In this final Gem we look back over some highlights of the series, including the topics covered and your favorite Gems. We also look to the future…
Johannes Kanig
Explicit Assumptions in SPARK 2014
In this article, we provide a short introduction to our paper at the Test and Proof 2014 conference in York, UK.
Claire Dross
External Axiomatizations: a Trip Into SPARK’s Internals
There are cases expressing all the specification of a package in SPARK is either impossible (for example if you need to link them to elements of the…
Claire Dross
Manual Proof with Ghost Code in SPARK 2014
Guiding automatic solvers by adding intermediate assertions is a commonly used technique. We can go further in this direction, by adding complete…
Gem #160 : Developing unit tests with GNATtest
No one likes to spend the time on testing. It's tedious and boring writing the test harness, the tests themselves, and keeping them in sync with your…
Yannick Moy
Short Video Demo of SPARK 2014
New to SPARK? Want to "see" what's new in SPARK 2014? It's all in this 5 mn video demo!
Gem #159 : GPRinstall - Part 2
GPRinstall is a tool recently developed by AdaCore that provides an easy way to install a project, whether it be a standard project, a library…