Blog
An Insight Into the AdaCore Ecosystem
Formal Methods Practice and Theory
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
Bitcoin blockchain in Ada: Lady Ada meets Satoshi Nakamoto
Felix Krause
The Road to a Thick OpenGL Binding for Ada: Part 1
Pierre-Marie de Rodat, Yannick Moy, Fabien Chouteau, Raphaël Amiard