Blog
An Insight Into the AdaCore Ecosystem
Formally Verified Hashed Sets in Ada SPARK
Fabien Chouteau
Ada GameDev Part 1: GEneric Sprite and Tile Engine (GESTE)
In this first entry of the series, I want to present my GEneric Sprite and Tile Engine (GESTE) project. The goal of GESTE is to bring the rendering…
Yannick Moy, Claire Dross
Proving the Correctness of GNAT Light Runtime Library
The GNAT light runtime library is a version of the runtime library targeted at embedded platforms and certification, which has been certified for use…
Quentin Ochem, Florian Gilcher
AdaCore and Ferrous Systems Joining Forces to Support Rust
Fabien Chouteau
AdaCore at FOSDEM 2022
Fabien Chouteau
Ada/SPARK Crate Of The Year 2021 Winners Announced!
Yannick Moy
SPARKNaCl - Two Years of Optimizing Crypto Code in SPARK (and counting)
SPARKNaCl is a SPARK version of the TweetNaCl cryptographic library, developed by formal methods and security expert Rod Chapman. For two years…
Paul Butcher
Fuzz Testing in International Aerospace Guidelines
Through the HICLASS UK research group, AdaCore has been developing security-focused software development tools that are aligned with the objectives…
Fabien Chouteau
An Embedded USB Device stack in Ada
A couple years ago I started to tackle what was probably my most daunting project at the time, an embedded USB Device stack written 100% in Ada.
Fabien Chouteau
Starting micro-controller Ada drivers in the Alire ecosystem
A few days ago, someone asked on the Ada Drivers Library repository how to add support for the SAMD21 micro-controller. Nowadays, I would rather…
Yannick Moy
Enhancing the Security of a TCP Stack with SPARK
The developers of CycloneTCP library at Oryx Embedded partnered with AdaCore to replace the TCP part of the C codebase by SPARK code, and used the…
Pat Rogers
Task Suspension with a Timeout in Ravenscar/Jorvik
This blog entry shows how to define an abstract data type that allows tasks to block on objects of the type, waiting for resumption signals from…
Fabien Chouteau
A design pattern for OOP in Ada
When I do Object Oriented Programming with Ada, I tend to follow a design pattern that makes it easier for me and hopefully also for people reading…