AdaCore: Build Software that Matters
AdaCore Hero Image

Blog

An Insight Into the AdaCore Ecosystem

I Stock 1160007422
Dec 01, 2025
Fabien Chouteau

Announcing Advent of Ada/SPARK 2025: Coding for a Cause!

Advent of Ada/SPARK is back! Solve Advent of Code 2025 challenges in Ada/SPARK and help us raise up to $5,000 for Ada Developers Academy.
Read More
Adacore card default
Nov 16, 2017

Yannick Moy, Martin Becker, Emanuel Regnath

Physical Units Pass the Generic Test

The support for physical units in programming languages is a long-standing issue, which very few languages have even attempted to solve. This issue…

Ada motorcontrol 1
Nov 14, 2017

Jonas Attertun

Make with Ada 2017: Brushless DC Motor Controller

This project involves the design of a software platform that provides a good basis when developing motor controllers for brushless DC motors…

Adacore card default
Oct 18, 2017

Yannick Moy

Prove in the Cloud

We have put together a byte (8 bits) of examples of SPARK code on a server in the cloud. The benefit with this webpage is that anyone can now…

Adacore card default
Sep 12, 2017

Yannick Moy

SPARK Tutorial at FDL Conference

Researcher Martin Becker is giving a SPARK tutorial next week at FDL conference. This post gives a link to his tutorial material (cookbook and…

Adacore card default
Aug 24, 2017

Yannick Moy

New SPARK Cheat Sheet

Our good friend Martin Becker has produced a new cheat sheet for SPARK, that you may find useful for a quick reminder on syntax that you have not…

I Stock 516257332
Aug 08, 2017

Pierre-Marie de Rodat

Highlighting Ada with Libadalang

Adacore card default
Jul 25, 2017

Pierre-Marie de Rodat

Pretty-Printing Ada Containers with GDB Scripts

Adacore card default
Jul 20, 2017

Yannick Moy

Proving Loops Without Loop Invariants

For all the power that comes with proof technology, one sometimes has to pay the price of writing a loop invariant. Along the years, we've strived to…

Adacore card default
Jul 18, 2017

Yannick Moy

Research Corner - Focused Certification of SPARK in Coq

The SPARK toolset aims at giving guarantees to its users about the properties of the software analyzed, be it absence of runtime errors or more…

Adacore card default
Jun 29, 2017

Yannick Moy

Applied Formal Logic: Searching in Strings

A friend pointed me to recent posts by Tommy M. McGuire, in which he describes how Frama-C can be used to functionally prove a brute force version of…

Adaroombot cover
Jun 20, 2017

Rob Tice

The Adaroombot Project

The Adaroombot project consists of an iRobot CreateⓇ 2 and Ada running on a Raspberry Pi with a Linux OS. This is a great Intro-to-Ada project as it…

Adacore card default
Jun 15, 2017

Pierre-Marie de Rodat, Nicolas Setton

GNAT GPL 2017 is out!