Blog
An Insight Into the AdaCore Ecosystem
Formally Verified Hashed Sets in Ada SPARK
Thomas Quinot
PolyORB now lives on Github
Rob Tice
SPARKZumo Part 2: Integrating the Arduino Build Environment Into GPS
This is part #2 of the SPARKZumo series of blog posts. This post covers the build system that was used to build the SPARKZumo project and how to…
Fabien Chouteau, Yannick Moy, Vasiliy Fofanov, Nicolas Setton
A Modern Syntax for Ada
One of the most criticized aspect of the Ada language throughout the years has been its outdated syntax. Fortunately, AdaCore decided to tackle this…
Fabien Chouteau
Getting Rid of Rust with Ada
There are a lot of DIY CNC projects out there (router, laser, 3D printer, egg drawing, etc.), but I never saw a DIY CNC sandblaster. So I decided to…
Rob Tice
SPARKZumo Part 1: Ada and SPARK on Any Platform
Yannick Moy
Two Days Dedicated to Sound Static Analysis for Security
AdaCore has been working with CEA, Inria and NIST to organize a two-days event dedicated to sound static analysis techniques and tools, and how they…
Yannick Moy
Secure Software Architectures Based on Genode + SPARK
SPARK user Alexander Senier presented recently at BOB Konferenz in Germany their use of SPARK for building secure mobile architectures. What's nice…
Fabien Chouteau
Ada on the micro:bit
Yannick Moy
Tokeneer Fully Verified with SPARK 2014
Tokeneer is a software for controlling physical access to a secure enclave by means of a fingerprint sensor. This software was created by Altran…
Felix Krause
The Road to a Thick OpenGL Binding for Ada: Part 2
This blog post is part two of a tutorial based on the OpenGLAda project and will cover implementation details such as a type system for interfacing…
Yannick Moy
For All Properties, There Exists a Proof
With the recent addition of a Manual Proof capability in SPARK 18, it is worth looking at an example which cannot be proved by automatic provers, to…
Johannes Kanig