Blog

Isabelle Vialard

Secure Use of Cryptographic Libraries: SPARK Binding for Libsodium

The challenge faced by cryptography APIs is to make building functional and secure programs easy for the user. In this blog post I will present you…

Joffrey Huguet, Johannes Kanig

Proving a simple program doing I/O ... with SPARK

The functionality of many security-critical programs is directly related to Input/Output (I/O). This includes command-line utilities such as gzip,…

Juan Zamorano

Using Ada for a Spanish Satellite Project

Yannick Moy, Raphaël Amiard, Tucker Taft

RFCs for Ada and SPARK evolution now on GitHub

Interested in participating in the evolution of the Ada or SPARK languages? We have something for you.

Claire Dross

Using Pointers in SPARK

In this blog post, I will present one of the most interesting additions to the community 2019 version of SPARK: pointer support. One of the core…

Nicolas Setton

GNAT Community 2019 is here!

Boran Car

Bringing Ada To MultiZone

C is the dominant language of the embedded world, almost to the point of exclusivity. Due to its age, and its goal of being a “portable assembler”,…

Allan Ascanius, Per Dalgas Jakobsen

Winning DTU RoboCup with Ada and SPARK

The Danish Technical University has a yearly RoboCup where autonomous vehicles solve a number of challenges. We participated with RoadRunner, a 3D…

Joffrey Huguet

Using SPARK to prove 255-bit Integer Arithmetic from Curve25519

Pamela Trevino

Public Ada Training Paris June 3-7, 2019

Arnaud Charlet

How Do We Use CodePeer at AdaCore

Peter Chapin

Ten Years of Using SPARK to Build CubeSat Nano Satellites With Students

My colleague, Carl Brandon, and I have been running the CubeSat Laboratory at Vermont Technical College (VTC) for over ten years. During that time we…