Blog
An Insight Into the AdaCore Ecosystem
Proving Safety at Scale: SPARK, RISC-V, and NVIDIA’s Security Strategy
Read More
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…
Yannick Moy
When the RISC-V ISA is the Weakest Link
Kyriakos Georgiou
Security-Hardening Software Libraries with Ada and SPARK
Fabien Chouteau
Announcing The First Ada/SPARK Crate Of The Year Award
We're happy to announce our new programming competition, the Ada/SPARK Crate Of The Year Award! We believe the Alire package manager is a game…
Roderick Chapman
SPARKNaCl with GNAT and SPARK Community 2021: Port, Proof and Performance
This post continues our adventures with SPARKNaCl - our verified SPARK version of the TweetNaCl cryptographic library. This time, we'll be looking at…
Jessie Glockner
Celebrating Women Engineering Heroes - International Women in Engineering Day 2021
Arnaud Charlet
Going beyond Ada 2022
Fabien Chouteau, Nicolas Setton
GNAT Community 2021 is here!
Pat Rogers
An Introduction to Jorvik, the New Tasking Profile in Ada 2022
The Ada 2022 draft defines a new tasking profile named Jorvik (pronounced “Yourvick”), based directly on the standard Ravenscar profile. Jorvik…
Fabien Chouteau
From Rust to SPARK: Formally Proven Bip-Buffers
I am following the evolution of the embedded Rust community and in particular the work of James Munns from Ferrous-Systems. One of the projects that…
Pat Rogers