Blog

Alexander Senier

RecordFlux: From Message Specifications to SPARK Code

Handling binary data is hard. Errors in parsers routinely lead to critical security vulnerabilities. In this post we show how the RecordFlux toolset…

Arnaud Charlet

The Power of Technology Integration and Open Source

Michael Frank

Learning SPARK via Conway's Game of Life

How I learned to write SPARK-provable code using Conway's Game Of Life

Claire Dross

Pointer Based Data-Structures in SPARK

As seen in a previous post, it is possible to use pointers (or access types) in SPARK provided the program abides by a strict memory ownership policy…

Arnaud Charlet

Combining GNAT with LLVM

Emma Adby

The Make with Ada competition is back!

Maxim Reznik, Yannick Moy

First Ada Virtual Conference organized by and for the Ada community

The Ada Community has gathered recently around a new exciting initiative - an Ada Virtual Conference, to present Ada-related topics in a 100% remote…

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…