Blog
An Insight Into the AdaCore Ecosystem
Getting Started in Functional Safety with Rust
Manuel Hatzl
SPARK Crate of the Year: Unbounded containers in SPARK
Manuel Hatzl is the winner of the 2021 SPARK Crate of the year! In this blog post he shares his experience using Ada/SPARK and how he created the…
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…