Blog

Claire Dross

Handling Aliasing through Pointers in SPARK

Fabien Chouteau, Joffrey Huguet

Quite Proved Image Format

A few weeks ago a piece of code went viral in the online dev community. The “Quite OK Image Format” (QOI) is a fast, lossless image compression…

Fabien Chouteau

Ada GameDev Part 2: Making 2D maps with Tiled

In this second post of the Ada GameDev series we will see how to create game maps and export them to a format that is compatible with the GESTE…

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 ver­sion of the Tweet­Na­Cl cryp­to­graph­ic 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.