298 entries tagged with #Ada
by Thomas Couderc
From Desert Dunes to Humanitarian Aid: Inside the Epic Journey of the 4L Trophy Rally
Back in February 2023, my friend David and I embarked on an exciting journey for a worthy cause. We finally got our old Renault 4l fully restored by ourselves and heard the engine revving for the first time one week before the departure.by Fabien Chouteau
RecordFlux State Machines
In a previous post we presented the RecordFlux specification language and toolset, illustrating how to design and generate formally proven binary protocol parsers and serializers. In this follow-up we will look at the protocol session part of RecordFlux.by Nicolas Setton
Reducing Ada code bases with adareducer
How we're using Libadalang to create an automated Ada code reducer.by Yannick Moy
The Case for SPARK Evolution - an April First Parable
SPARK already allows you to specify functional contracts by cases, and soon it will allow you to specify cases that lead to an exception. But what about all the other cases? Should we put all our eggs in the same case? Discover what's cooking up for you on the side of language evolution.by Fabien Chouteau
The End of Binary Protocol Parser Vulnerabilities
This week we announced a new tool called RecordFlux. The goal of RecordFlux is to address one of the most critical parts of the software stack in terms of security, binary protocol parsers/serializers.From a protocol specification written in the RecordFlux Domain Specific Language (DSL), the tool can generate provable SPARK code. This means memory safety (no buffer overruns), absence of integer overflow errors, and even proof of functional properties. In this blog post I will try to explain how this is a game changer for cybersecurity.by Maxim Reznik
Introduction to VSS library
The VSS (as an abbreviation for Virtual String Subsystem) library is designed to provide advanced string and text processing capabilities. It offers a convenient and robust API that allows developers to work with Unicode text, regardless of its internal representation. In this article, we will introduce you to the library and explain its purpose, highlighting its usefulness for developers working in this area.by Fabien Chouteau
GNAT Pro 21.6 for LYNX MOSA.ic for Avionics (MfA)
AdaCore has partnered closely with Lynx to deliver Ada language support alongside its LYNX MOSA.ic software framework that comprises a real-time operating system (LynxOS-178), Linux and hypervisor (LynxSecure) technology.
by Paul Butcher
Automated Assurance through Differential Fuzzing
This blog describes the concept and benefits of differential fuzz testing. In addition, the post describes setting up, executing and analyzing the results of a differential fuzzing campaign for the Libkeccak and XKCP cryptographic libraries.by Fabien Chouteau
AdaCore joins the Rust foundation
Last year we announced our strategic partnership with Ferrous Systems, a technology company specializing in the Rust programming language. Today we are announcing a new step in our involvement with the Rust ecosystem and communityby Fabien Chouteau
AdaCore at FOSDEM 2023
This year marks the return of the FOSDEM conference as an "in-person" event. As always, AdaCore will participate in this major gathering of the free and open source community.We encourage you to stop by the Ada-Europe booth (Building K, level 2) to have a chat or get answers to any questions regarding Ada, SPARK, or other topics, such as those covered in our blog.
by Fabien Chouteau
Ada/SPARK Crate Of The Year 2022 Winners Announced!
In June of 2022 we launched the second edition of the Ada/SPARK Crate Of The Year Awards. We believe the Alire source package manager is a game changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem. Today we are pleased to announce the results. But first, we want to congratulate all the participants, and the Alire community at large, for reaching 320 crates in the ecosystem in January of this year. We truly believe in a bright future for the Ada/SPARK open-source ecosystem with Alire at the forefront. Reaching this milestone is a great sign,both inside and outside the Ada/SPARK community, of the evolution and the energy of the ecosystem.
by Fabien Chouteau

Advent of Ada/SPARK 2022 Results
At the end of November we called the Ada and SPARK programmers community to take on a challenge for a good cause. We are now in January and it is time for the results!by Fabien Chouteau

Our Contribution to the Ada Logo Discussion
From time to time we see, here and there, discussions in the Ada community about the design and adoption of a common logo to represent the language. Today we want to bring our contribution to this discussion by offering a logo to the Ada community.by Fabien Chouteau

Coroutines in Ada, a Clean but Heavy Implementation
A few months ago I was reading this article about coroutines in game development and how they are great tools for writing scripts (as in movie scripts) in the same language as the game engine. Until then I heard about coroutines but never really gave them a thought, this piqued my curiosity.by Pat Rogers
New Learn Course: Introduction To Embedded Systems Programming
A new online Learn course has been published offering an Introduction To Embedded Systems Programming.
by Fabien Chouteau
Tis the Season to be Giving falalalala lalalala
Every year since 2015, a team of dedicated individuals led by Eric Wastl organizes an online programming challenge called: Advent of Code. The concept is simple yet brilliant: from December 1st to 25th, every day a new small programming exercise is published on the adventofcode.com website. This year we want to join the fun, and bring a little bit of extra motivation for a good cause.by Fabien Chouteau
NVIDIA Security Team: “What if we just stopped using C?”
Today I want to share a great story about why many NVIDIA products are now running formally verified SPARK code. This blog post is in part a teaser for the case study that NVIDIA and AdaCore published today. Our journey begins with the NVIDIA Security Team. Like many other security oriented teams in our industry today, they were looking for a measurable answer to the increasingly hostile cybersecurity environment and started questioning their software development and verification strategies.by Daniel King
Avoiding Vulnerabilities in Crypto Code with SPARK
Writing secure software in C is hard. It takes just one missed edge case to lead to a serious security vulnerability, and finding such edge cases is difficult. This blog post discusses a recent vulnerability in a popular SHA-3 library and how the same problems were avoided in my own SHA-3 library written in SPARK.
by Johannes Kliemann
Adding Ada to Rust
While implementing application logic in Ada or SPARK is an improvement over a pure C project, its weakest link is still the C code in the SDK. On the other hand, there are many libraries, board support packages, and SDKs written in Rust, easily usable with Cargo. So instead of building the Ada application on top of a C base, one could use a Rust base instead to combine the large catalog of ready-to-use software with Rust's safety features, providing a much more solid base for an Ada project.by Andry Ogorodnik

New features for string literals and comments in GNAT Studio
We have added several new convenience features that help work with comments and string literals in Ada code.by Paul Butcher
Fuzzing Out Bugs in Safety-Critical Embedded Software
Fuzzing Out Bugs in Safety-Critical Embedded Software: Paul Butcher from AdaCore talks to Brandon Lewis from Embedded Toolboxby Fabien Chouteau

Embedded Ada/SPARK, There's a Shortcut
For years in this blog my colleagues and I have published examples, demos, and how-to’s on Ada/SPARK embedded (as in bare-metal) development. Most of the time, if not always, we focused on one way of doing things: to start from scratch and write everything in Ada/SPARK, from the low level drivers to the application. While this way of doing Ada/SPARK embedded will yield the best results in terms of software quality, it might not be the most efficient in all cases. In this blog post I want to present an alternative method to introduce Ada/SPARK into your embedded development projects.by Paul Butcher
Join us at the High Integrity Software (HIS) Conference 2022!
After two years of virtual events, we are very happy to report that the High Integrity Software Conference (HIS) will be making a physical comeback on Tuesday 11th October 2022 at the Bristol Marriott Hotel City Centre, Bristol, UK. Since 2014, AdaCore has been co-organising the event with Capgemini Engineering (previously known as Altran Technologies, SA). The success and growth of the conference have ensured it remains a regular fixture for returning delegates, and the exciting lineup for this year's event will ensure HIS 2022 is no exception!
by Quentin Ochem
Announcing Publication of the Draft Ferrocene Language Specification
We are pleased to announce the publication of the initial draft of the Ferrocene Language Specification (FLS) - a qualification-oriented document that details the Rust language as it specifically relates to Ferrocene.by Fabien Chouteau
Announcing The 2022 Ada/SPARK Crate Of The Year Award
We're happy to announce our the second edition of our programming competition, the Ada/SPARK Crate Of The Year Award! We believe the Alire package manager is a game changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem.by Yannick Moy , Lionel Matias

I can’t believe that I can prove that it can sort
When an enthusiastic Ada programmer and a SPARK expert pair up to prove the most "stupid" sorting algorithm, lessons are learned! Join us in this eye-opening journey.by Fabien Chouteau
A New Era For Ada/SPARK Open Source Community
Today we have two exciting announcements for the future of the Ada/SPARK ecosystem.by Gustavo A. Hoffmann
Announcing Updates to learn.adacore.com
by Paul Jarrett
Ada Crate of the Year: Interactive code search
A retrospective on learning Ada and developing a tool with it in 2021 from 2021 Ada Crate of the Year Winner Paul Jarrett.by Claire Dross
Handling Aliasing through Pointers in SPARK
As I explained in a blog post a couple of years ago, pointers are subjected to a strict ownership policy in SPARK. It prevents aliasing and allows for an efficient formal verification model. Of course, it comes at the cost of restrictions which might not be applicable to all usage. In particular, while ownership makes it possible to represent certain recursive data-structures, those involving cycles or sharing are de-facto forbidden. This is a choice, and not every proof tool did the same. For example, the WP plug-in of Frama-C supports pointers with arbitrary aliasing. If some information about the separation of memory cells is necessary to verify a program, then the user shall give the annotation explicitly. I have investigated modeling pointers with aliasing in SPARK as indices in a big memory array. I will present the results of my experiments in this blog post. We will see that, while such a representation is indeed possible modulo some hiding in SPARK, it can quickly become rather heavy in practice.
by 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 designed to have a very simple implementation (about 300 lines of C). Shortly, a few alternative implementations popped up here and there, and in this kind of situation we are eager to show what Ada/SPARK can bring to the table.by 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 library.by 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 spark_unbound libraryby 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 and anesthetic of 8bit era game consoles to modern microcontrollers.by 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 at the highest levels of criticality in several industrial domains. It contains around 180 units focused mostly on I/O, numerics, text manipulation, memory operations. We have used SPARK to prove the correctness of 40 of them: that the code is free of runtime errors, and that it satisfies its functional specifications.by Quentin Ochem , Florian Gilcher
AdaCore and Ferrous Systems Joining Forces to Support Rust
For over 25 years, AdaCore has been committed to supporting the needs of safety- and mission-critical industries. This started with an emphasis on the Ada programming language and its toolchain, and over the years has been extended to many other technologies. AdaCore’s product offerings today include support for the Ada language and its formally verifiable SPARK subset, C and C++, and Simulink and Stateflow models. We have accomplished this while addressing the requirements of various safety standards such as DO-178B/C, EN 50128, ECSS-E-ST-40C / ECSS-Q-ST-80C, IEC 61508 and ISO 26262.
by Fabien Chouteau
AdaCore at FOSDEM 2022
Like previous years, AdaCore will participate in FOSDEM. Once again the event will be online only, but this won’t prevent us from celebrating Open Source software and it is an opportunity for even more people to participate around the world.
by Fabien Chouteau
Ada/SPARK Crate Of The Year 2021 Winners Announced!
In June of 2021 we announced the launch of a new programming competition called Ada/SPARK Crate Of The Year Awards. We believe the Alire source package manager is a game changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem. Today we are pleased to announce the results. But first, we want to congratulate all the participants, and the Alire community at large, for reaching 200 crates in the ecosystem in January of this year. We truly believe in a bright future for the Ada/SPARK open-source ecosystem with Alire at the forefront. Reaching this milestone is a great sign, inside and outside the Ada/SPARK community, of the evolution and the energy of the ecosystem.
by 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 stated within the avionics security standards. In addition, they have been developing further guidelines that describe how vulnerability identification and security assurance activities can be described within a Plan for Security Aspects of Certification.by 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.by Fabien Chouteau
Starting micro-controller Ada drivers in the Alire ecosystem
A few days ago, someone asked on the Ada Drivers Library repository how to add support for the SAMD21 micro-controller. Nowadays, I would rather recommend people to contribute this kind of micro-controller support project to the Alire ecosystem. I started to write a few instructions on how to get started, but it quickly became a blog-worthy piece of text.by Yannick Moy
Enhancing the Security of a TCP Stack with SPARK
The developers of CycloneTCP library at Oryx Embedded partnered with AdaCore to replace the TCP part of the C codebase by SPARK code, and used the SPARK tools to prove both that the code is not vulnerable to the usual runtime errors (like buffer overflow) and that it correctly implements the TCP automaton specified in RFC 793. As part of this work, we found two subtle bugs related to memory management and concurrency. This work has been accepted for publication at the upcoming IEEE SecDev 2021 conference.by 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 other components, for at most a specified amount of time per object. This "timeout" capability has been available in Ada from the beginning, via select statements containing timed entry calls. But what about developers working within the Ravenscar and Jorvik tasking subsets? Select statements and timed calls are not included within either profile. This new abstraction will provide some of the functionality of timed entry calls, with an implementation consistent with the Ravenscar and Jorvik subsets.by 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 my code.by Kyriakos Georgiou
Security-Hardening Software Libraries with Ada and SPARK
Part of AdaCore's ongoing efforts under the HICLASS project is to demonstrate how the SPARK technology can play an integral part in the security-hardening of existing software libraries written in other non-security-oriented programming languages such as C. This blog post presents the first white paper under this work-stream, “Security-Hardening Software Libraries with Ada and SPARK”.
by 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 changer for Ada/SPARK, so we want to use this competition to reward the people contributing to the ecosystem.by 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 yet more performance improvement via proof-driven "operator narrowing", porting the library to GNAT Community 2021, and the effect that has on proof and performance of the code.by Jessie Glockner
Celebrating Women Engineering Heroes - International Women in Engineering Day 2021
Women make up roughly 38% of the global workforce, yet they constitute only 10–20% of the engineering workforce. In the U.S., numbers suggest that 40% of women who graduate with engineering degrees never enter the profession or eventually leave it. Why? The reasons vary but primarily involve socio-economic constraints on women in general, workplace inequities, and lack of support for work-life balance. Sadly, history itself has often failed to properly acknowledge the instrumental contributions of women inventors, scientists, and mathematicians who have helped solve some of our world's toughest challenges. How can young women emulate their successes if they don't even know about them?
by Arnaud Charlet
Going beyond Ada 2022
As we've seen previously in Ada 2022 support in GNAT, the support for Ada 2022 is now mostly there for everyone to take advantage of. We're now crossing fingers for this new revision to be officially stamped by ISO in 2022.
by Fabien Chouteau , Nicolas Setton

GNAT Community 2021 is here!
We are happy to announce that the GNAT Community 2021 release is now available via https://www.adacore.com/download. Here are some release highlights:
by 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 relaxes certain restrictions in order to increase expressive power for real-time/embedded Ada and SPARK applications. We will explore the details in this blog entry.by 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 caught my attention is bbqueue, a single producer, single consumer, lockless, thread safe queue, based on BipBuffers.by Pat Rogers
On the Benefits of Families ... (Entry Families)
Ada has a concurrency construct known as “entry families” that, in some cases, is just what we need to express a concise, clear solution.
by Simon Buist

Showing Global contracts with GNAT Studio
In the integrated development environment, GNAT Studio, there is now a plugin that inserts the generated Global contracts inline with the code.by Roderick Chapman
Doubling the Performance of SPARKNaCl (again...)
Following my last blog entry, further experiments show how the performance of SPARKNaCl can be doubled (again), plus analysis of worst-case stack usage and code size at all optimization levels.by Roderick Chapman
Performance analysis and tuning of SPARKNaCl
This blog goes into the details of both measuring and improving the runtime performance of SPARKNaCl on a real "bare metal" embedded target, and comparing results with those for the original "TweetNaCl" C implementation.by Fabien Chouteau
AdaCore at FOSDEM 2021
Like previous years, AdaCore will participate in FOSDEM. This time the event will be online only, but this won’t prevent us from celebrating Open Source software. AdaCore engineers will give two talks in the Safety and Open Source devroom, a topic at the heart of AdaCore since its inception.by Fabien Chouteau

Mini SAM M4 Ada BSP
Beyond the great look, the Mini SAM M4 provide a powerful 120 Mhz Microchip SAMD51 Cortex-M microcontroller, a couple of LEDs and a user button. Let's program it with Ada.by Léo Germond
How To: GNAT Pro with Docker
Using GNAT Pro with containerization technologies, such as Docker, is so easy, a whale could do it!
by Fabien Chouteau
Ada on any ARM Cortex-M device, in just a couple minutes
In this blog post I want to present a new tool that allows one to very quickly and easily start Ada programming on any ARM Cortex-M or RISC-V microcontroller.by Paul Butcher
Finding Vulnerabilities using Advanced Fuzz testing and AFLplusplus v3.0
Some of you may recall an AdaCore blog post written in 2017 by Thales engineer Lionel Matias titled "Leveraging Ada Run-Time Checks with Fuzz Testing in AFL". This insightful post took us on a journey of discovery as Lionel demonstrated how Ada programs, compiled using GNAT Pro and an adapted assembler pass can be subjected to advanced fuzz testing. In order to achieve this Lionel demonstrated how instrumentation of the generated assembly code around jump and label instructions, could be subjected to grey-box (path aware) fuzz testing (using the original AFL v2.52b as the fuzz engine). Lionel explained how applying the comprehensive spectrum of Ada runtime checks, in conjunction with Ada's strong typing and contract based programming, enhanced the capabilities of fuzz testing beyond the abilities of other languages. Ada's advanced runtime checking, for exceptions like overflows, and the scrutiny of Ada's design by contract assertions allow corner case bugs to be found whilst also utilising fuzz testing to verify functional correctness.
by Juliana Silva

Make with Ada 2020: ADArrose
Charles Villard, Cyril Etourneau, Thomas Delecroix, Louise Flick worked together in the ADArrose project. It won the student prize in the Make with Ada 2019/20 competition. This project was originally posted on Hackster.io here. For those interested in participating in the 2020/21 competition, registration is now open and project submissions will be accepted until Jan 31st 2021, register here.
by Juliana Silva

Make with Ada 2020: The autonomous firetruck
The AFT (Autonomous FireTruck) is a prototype of an autonomous firetruck that can put out fire without risking people's lives. This project won a finalist prize in the Make with Ada 2019/20 competition.by Juliana Silva

Make with Ada 2020: Ada Robot Car With Neural Network
Guillermo Perez's project won a finalist prize in the Make with Ada 2019/20 competition. This project was originally posted on Hackster.io here. For those interested in participating in the 2020/21 competition, registration is now open and project submissions will be accepted until Jan 31st 2021, register here.by Fabien Chouteau

Ada for micro:bit Part 8: Music to my ears
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
by Fabien Chouteau
First beta release of Alire, the package manager for Ada/SPARK
A few years ago we realized that having a package manager for the Ada/SPARK community would be a game changer. Since then, AdaCore has been sponsoring and contributing to the Alire project created by Alejandro Mosteo from the Centro Universitario de la Defensa de Zaragoza. With this blog post I want to introduce Alire and explain why this project is important for the `Ada`/`SPARK` community.by Arnaud Charlet
Ada 202x support in GNAT
News from the Ada front The next revision of the Ada standard is now almost ready, so it's time for a status update on where GNAT and AdaCore stand on this front!
by Juliana Silva

Make With Ada 2020: High Integrity Sumobot
Blaine Osepchuk's project won a finalist prize in the Make with Ada 2019/20 competition. This project was originally posted on Hackster.io here. For those interested in participating in the 2020/21 competition, registration is now open and project submissions will be accepted until Jan 31st 2021, register here.
by Fabien Chouteau

Ada for micro:bit Part 7: Accelerometer
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
by Juliana Silva

Make with Ada 2020: CHIP-8 Interpreter
Laurent Zhu's and Damien Grisonnet's project was accomplished for the EPITA Ada courses and won a finalist prize in the Make with Ada 2019/20 competition.by Fabien Chouteau

Ada for micro:bit Part 6: Analog Input
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
by Fabien Chouteau

Ada for micro:bit Part 5: Analog Output
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
by Fabien Chouteau

Ada for micro:bit Part 4: Pin Input
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
by Fabien Chouteau , Emma Adby
AdaCore Code of Conduct
Starting today, AdaCore has put in place a Code of Conduct (CoC) to ensure a positive environment for everyone willing and wanting to interact with us. With the development of this blog, our twitter accounts, and our GitHub corporate account, there is more and more communication between AdaCore and a number of communities. In this Code of Conduct we want to explain how we are going to moderate the AdaCore-maintained community spaces with the goal of maintaining a welcoming, friendly environment.
by Fabien Chouteau

Ada for micro:bit Part 3: Pin Output
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.by Michael Frank

Code Obfuscator for Ada using Libadalang and SPARK
A code obfuscator is a method of sharing coding discussions of real-world examples without giving away proprietary or classified information. This article shows an example of an Ada obfuscator, written in the SPARK language and using the Libadalang library to intelligently hide names and text within the source.by Fabien Chouteau

Ada for micro:bit Part 2: Push buttons
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
by Fabien Chouteau

Ada for micro:bit Part 1: Getting Started
Welcome to the Ada for micro:bit series where we look at simple examples to learn how to program the BBC micro:bit with Ada.
by Pierre-Marie de Rodat
GNATcoverage: getting started with instrumentation
This is the second post of a series about GNATcoverage and source code instrumentation. The previous post introduced how GNATcoverage worked originally and why we extended it to support source instrumentation-based code coverage computation. Let’s now see it in action in the most simple case: a basic program running on the host machine, i.e. the Linux/Windows machine that runs GNATcoverage itself.
by Pierre-Marie de Rodat
Introducing source code instrumentation in GNATcoverage
This is the first post of a series about GNATcoverage and source code instrumentation.In order to make GNATcoverage viable in more contexts, we planned several years ago to add instrumentation support in GNATcoverage for Ada sources. This feature reached maturation recently and is available in the last Continuous Release, so it is a good time to present it with a blog series!by Jessie Glockner , Ben Brosgol
The FACE™ open systems strategy gaining traction in the avionics industry
The FACE™ approach is a government-industry initiative for reducing defense system life cycle costs through portable and reusable software components. It consists of a technical approach — a software standard based on well-defined common interfaces — and a business strategy for encouraging the development and deployment of FACE conformant products.by Emma Adby

Make with Ada 2020: LoRaDa := Ada + LoRa;
Hedley Rainnie's project combines 6 different SoCs all programmed in Ada performing as a LoRa network. He also showcases a BLE bridge to a LoRa server. His project came about when him and his wife were musing about how to detect and deter unwanted garden visitors. This ongoing project won a finalist prize in the 2019/20 Make with Ada competition.by Claire Dross
Relaxing the Data Initialization Policy of SPARK
SPARK always being under development, new language features make it in every release of the tool, be they previously unsupported Ada features (like access types) or SPARK specific developments. However, new features generally take a while to make it into actual user code. The feature I am going to present here is in my experience an exception, as it was used both internally and by external users before it made it into any actual release. It was designed to enhance the verification of data initialization, whose limitations have been a long standing issue in SPARK.by Emma Adby

Make with Ada 2020: Disaster Management with Smart Circuit Breaker
Shahariar's project ensures safety against electrical fire or shock during an earthquake, flood, gas leakage or fire breakout by disconnecting the mains with a smart circuit breaker. Additionally, this project won a finalist prize in the 2019/20 Make with Ada competition.by Emma Adby

Make with Ada 2020: CryptAda - (Nuclear) Crypto on Embedded Device
Team CryptAda's project collects entropy, manages an entropy pool, implements a homemade PRNG, and generates RSA keys directly on the board with an accent on security. Additionally, this project won a finalist prize in the 2019/20 Make with Ada competition.by Emma Adby

Make with Ada 2020: The SmartBase - IoT Adjustable Bed
John Singleton's The SmartBase makes your existing adjustable bed safer and easier to use by adding voice control and safe (and fun!) LED underbed lighting! Additionally, this project won first place prize in the 2019/20 Make with Ada competition.by Jon Andrew
CuBit: A General-Purpose Operating System in SPARK/Ada
Last year, I started evaluating programming languages for a formally-verified operating system. I've been developing software for a while, but only recently began work in high integrity software development and formal methods. There are several operating system projects, like the SeL4 microkernel and the Muen separation kernel, that make use of formal verification. But I was interested in using a formally-verified language to write a general-purpose OS - an environment for abstracting the underlying hardware while acting as an arbiter for running the normal applications we're used to.by Nicolas Setton

GNAT Community 2020 is here!
We are happy to announce that the GNAT Community 2020 release is now available! Read the post for access to download and to find out about this year's release highlights.by Pat Rogers
From Ada to Platinum SPARK: A Case Study for Reusable Bounded Stacks
This blog entry describes the transformation of an Ada stack ADT into a completely proven SPARK implementation that relies on static verification instead of run-time enforcement of the abstraction’s semantics. We will prove that there are no reads of unassigned variables, no array indexing errors, no range errors, no numeric overflow errors, no attempts to push onto a full stack, no attempts to pop from an empty stack, that subprogram bodies implement their functional requirements, and so on. As a result, we get a maximally robust implementation of a reusable stack abstraction providing all the facilities required for production use.by Abe Cohen
An Introduction to Contract-Based Programming in Ada
One of the most powerful features of Ada 2012* is the ability to specify contracts on your code. Contracts describe conditions that must be satisfied upon entry (preconditions) and upon exit (postconditions) of your subprogram. Preconditions describe the context in which the subprogram must be called, and postconditions describe conditions that will be adhered to by the subprogram’s implementation. If you think about it, contracts are a natural evolution of Ada’s core design principle. To encourage developers to be as explicit as possible with their expressions, putting both the compiler/toolchain and other developers in the best position to help them develop better code.
by Johannes Kliemann
Ada on the ESP8266
Not long ago, AdaCore published its LLVM frontend for GNAT. Also quite recently Espressif updated their LLVM backend to LLVM 9 which also happens to be the LLVM version of GNAT. This gave me to the idea to try out if LLVMs promise of providing modular and reusable toolchain technologies is true.by Martyn Pike
A Trivial File Transfer Protocol Server written in Ada
For an upcoming project, I needed a simple way of transferring binary files over an Ethernet connection with minimal (if any at all) user interaction. A protocol that's particularly appropriate for this kind of usage is the Trivial File Transfer Protocol (TFTP).by Roderick Chapman
Proving properties of constant-time crypto code in SPARKNaCl
Over the last few months, I developed a SPARK version of the TweetNaCl cryptographic library. This was made public on GitHub in February 2020, under the 2-clause BSD licence. This blog entry goes into a bit more technical detail on one particular aspect of the project: the challenge of re-writing and verifying "constant time" algorithms using SPARK.by Ghjuvan Lacambre

Time travel debugging in GNAT Studio with GDB and RR
Learn how to use GDB and RR's advanced time traveling features in GNAT Studio.by Maxim Reznik
Android application with Ada and WebAssembly
Having previously shown how to create a Web application in Ada, it's not so difficult to create an Android application in Ada. Perhaps the simplest way is to install Android Studio. Then just create a new project and choose "Empty Activity". Open the layout, delete TextView and put WebView instead.
by Pat Rogers

Making an RC Car with Ada and SPARK
As a demonstration for the use of Ada and SPARK in very small embedded targets, I created a remote-controlled (RC) car using Lego NXT Mindstorms motors and sensors but without using the Lego computer or Lego software. I used an ARM Cortex System-on-Chip board for the computer, and all the code -- the control program, the device drivers, everything -- is written in Ada. Over time, I’ve upgraded some of the code to be in SPARK. This blog post describes the hardware, the software, the SPARK upgrades, and the repositories that are used and created for this purpose.
by Pierre-Marie de Rodat
A Further Expedition into Libadalang: Save Time with Libadalang.Helpers.App
Martyn’s recent blog post showed small programs based on Libadalang to find uses of access types in Ada sources. Albeit short, these programs need to take care of all the tedious logistics around processing Ada sources: find the files to work on, create a Libadalang analysis context, use it to read the source files, etc. Besides, they are not very convenient to run:
by Vadim Godunko
Using GNAT-LLVM to target Ada to WebAssembly
The GNAT-LLVM project provides an opportunity to port Ada to new platforms, one of which is WebAssembly. We conducted an experiment to evaluate the porting of Ada and the development of bindings to use Web API provided by the browser directly from Ada applications.
by Fabien Chouteau
AdaCore at FOSDEM 2020
Like last year and the year before, AdaCore will participate to the celebration of Open Source software at FOSDEM. It is always a key event for the Ada/SPARK community and we are looking forward to meet Ada enthusiasts. You can check the program of the Ada/SPARK devroom here.
by Fabien Chouteau

Ada on a Feather
I was quite happy to see AdaFruit release their first Feather format board including a micro-controller with plenty of Ada support, the STM32F4. I bought a board right away and implemented some support code for it.by Quentin Ochem
Witnessing the Emergence of a New Ada Era
For nearly four decades the Ada language (in all versions of the standard) has been helping developers meet the most stringent reliability, safety and security requirements in the embedded market. As such, Ada has become an entrenched player in its historic A&D niche, where its technical advantages are recognized and well understood. Ada has also seen usage in other domains (such as medical and transportation) but its penetration has progressed at a somewhat slower pace. In these other markets Ada stands in particular contrast with the C language, which, although suffering from extremely well known and documented flaws, remains a strong and seldom questioned default choice. Or at least, when it’s not the choice, C is still the starting point (a gateway drug?) for alternatives such as C++ or Java, which in the end still lack the software engineering benefits that Ada embodies..
by Paul Butcher
AdaCore for HICLASS - Enabling the Development of Complex and Secure Aerospace Systems
What's changed?In 2019 AdaCore created a UK business unit and embarked on a new and collaborative venture researching and developing advanced UK aerospace systems. This blog introduces the reader to ‘HICLASS’, describes our involvement and explains how participation in this project is aligned with AdaCore’s core values.
by Martyn Pike
An Expedition into Libadalang
I’ve been telling Ada developers for a while now that Libadalang will open up the possibility of more-easily writing Ada source code analysis tools. (You can read more about Libadalang here and here and can also access the project on Github.)
by 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 eases the creation of formally verified binary parsers in SPARK.by Arnaud Charlet
The Power of Technology Integration and Open Source
Part of our core expertise at AdaCore is to integrate multiple technologies as smoothly as possible and make it a product. This started at the very beginning of our company by integrating a code generator (GCC) with an Ada front-end (GNAT) which was then followed by integrating a debugger engine (GDB) and led to today's rich GNAT Pro offering.
by Michael Frank
Learning SPARK via Conway's Game of Life
How I learned to write SPARK-provable code using Conway's Game Of Lifeby 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 designed to prevent aliasing. We will show in this post how to define pointer-based data-structures in SPARK and how to traverse them without breaking the ownership policy.by Arnaud Charlet
Combining GNAT with LLVM
Presenting the GNAT LLVM projectAt AdaCore labs, we have been working for some time now on combining the GNAT Ada front-end with a different code generator than GCC.
by Emma Adby

The Make with Ada competition is back!
AdaCore’s fourth annual Make with Ada competition launched this week with over $8K in cash and prizes to be awarded for the most innovative embedded systems projects developed using Ada and/or SPARK.
by 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 event. The first such conference took place on August, 10th 2019, around the topic of the new features in Ada 202x. Here is what was presented.by 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 how I created a SPARK binding for Libsodium, using strong typing and preconditions/postconditions to enforce a safe and functional use of basic cryptographic primitives.by 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, which might process untrusted data downloaded from the internet, but also any servers that are directly connected to the internet, such as webservers, DNS servers and so on. In this blog post we show an approach that deals with error handling and reasoning about content, and demonstrate the approach using the cat command line utility.by Juan Zamorano
Using Ada for a Spanish Satellite Project
I am an Associate Professor at Polytechnic University of Madrid’s (Universidad Politécnica de Madrid / UPM) in the Department of Architecture and Technology of Computer Systems. For the past several years I have been directing a team of colleagues and students in the development of a UPMSat-2 microsatellite. The project originally started in 2013 as a follow-to the UPM-SAT 1, launched by an Ariane-4 in 1995.
by 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.by 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 assumption in SPARK has always been the absence of aliasing, so adding pointers without breaking this assumption was quite a challenge. I will explain how this was achieved using an ownership model for pointers (like is done in Rust) through small examples.by Nicolas Setton

GNAT Community 2019 is here!
We are pleased to announce that GNAT Community 2019 has been released! See https://www.adacore.com/download.
by 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”, it deliberately lacks type-safety, opening up exploit vectors. Proposed solutions are partitioning the application into smaller intercommunicating blocks, designed with the principle of least privilege in mind; and rewriting the application in a type-safe language. We believe that both approaches are complementary and want to show you how to combine separation and isolation provided by MultiZone together with iteratively rewriting parts in Ada. We will take the MultiZone SDK demo and rewrite one of the zones in Ada.by 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 printed robot with wheel suspension, based on the BeagleBone Blue ARM-based board and the Pixy 1 camera with custom firmware enabling real-time line detection. Code is written in Ada and formally proved correct with SPARK at Silver level.by Joffrey Huguet
Using SPARK to prove 255-bit Integer Arithmetic from Curve25519
In 2014, Adam Langley, a well-known cryptographer from Google, wrote a post on his personal blog, in which he tried to prove functions from curve25519-donna, one of his projects, using various verification tools: SPARK, Frama-C, Isabelle... He describes this attempt as "disappointing", because he could not manage to prove "simple" things, like absence of runtime errors. I will show in this blogpost that today, it is possible to prove what he wanted to prove, and even more.
by Pamela Trevino
Public Ada Training Paris June 3-7, 2019
This course is geared to software professionals looking for a practical introduction to the Ada language with a focus on embedded systems, including real-time features as well as critical features introduced in Ada 2012. By attending this course you will understand and know how to use Ada for both sequential and concurrent applications, through a combination of live lectures from AdaCore's expert instructors and hands-on workshops using AdaCore's latest GNAT technology. AdaCore will provide an Ada 2012 tool-chain and ARM-based target boards for embedded workshops. No previous experience with Ada is required.
by Arnaud Charlet
How Do We Use CodePeer at AdaCore
A question that our users sometimes ask us is "do you use CodePeer at AdaCore and if so, how?". The answer is yes! and this blog post will hopefully give you some insights into how we are doing it for our own needs.
by 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 have worked with nearly two dozen students on building and programming CubeSat nano satellites. Because of their general inexperience, and because of the high student turnover rate that is natural in an educational setting, our development process is often far from ideal. Here SPARK has been extremely valuable to us. What we lack in rigor of the development process we make up for in the rigor of the SPARK language and tools. In November 2013 we launched a low Earth orbiting CubeSat. The launch vehicle contained 13 other university built CubeSats. Most were never heard from. One worked for a few months. Ours worked for two years until it reentered Earth's atmosphere as planned in November 2015.by Yannick Moy , Nicolas Setton , Ben Brosgol
A Readable Introduction to Both MISRA C and SPARK Ada
MISRA C is the most widely known coding standard restricting the use of the C programming language for critical software. For good reasons. For one, its focus is entirely on avoiding error-prone programming features of the C programming language rather than on enforcing a particular programming style. In addition, a large majority of rules it defines are checkable automatically (116 rules out of the total 159 guidelines), and many tools are available to enforce those. As a coding standard, MISRA C even goes out of its way to define a consistent sub-language of C, with its own typing rules (called the "essential type model" in MISRA C) to make up for the lack of strong typing in C.
by Yannick Moy , Nicolas Roche , Pierre-Marie de Rodat , Fabien Chouteau
AdaCore at FOSDEM 2019
Like last year, we've sent a squad of AdaCore engineers to participate in the celebration of Open Source software at FOSDEM. Like last year, we had great interactions with the rest of the Ada and SPARK Community in the Ada devroom on Saturday. That's what we have to say about it.by Rob Tice
AdaFractal Part 2: Fixed Point and Floating Point Math Performance and Parallelization
In Part 1 of this blog post I discussed why I chose to implement this application using the Ada Web Server to serve the computed fractal to a web browser. In this part I will discuss a bit more about the backend of the application, the Ada part.
by Rob Tice
AdaFractal Part1: Ada with a Portable GUI
The is the first part of a multiple part post that covers the development of the AdaFractal project. The idea was to create fractals in Ada. Here we will cover how to use AWS to create a flexible and portable way to display the generated fractals without using bulky graphics libraries.by Quentin Ochem
NVIDIA is joining the Ada and SPARK adopter wave
Over the past several years, a great number of public announcements have been made about companies that are either studying or adopting the Ada and SPARK programming languages. Noteworthy examples include Dolby, Denso, LASP and Real Heart, as well as the French Security Agency.
by Quentin Ochem
Proving Memory Operations - A SPARK Journey
The promise behind the SPARK language is the ability to formally demonstrate properties in your code regardless of the input values that are supplied - as long as those values satisfy specified constraints. As such, this is quite different from static analysis tools such as our CodePeer or the typical offering available for e.g. the C language, which trade completeness for efficiency in the name of pragmatism. Indeed, the problem they’re trying to solve - finding bugs in existing applications - makes it impossible to be complete. Or, if completeness is achieved, then it is at the cost of massive amount of uncertainties (“false alarms”). SPARK takes a different approach. It requires the programmer to stay within the boundaries of a (relatively large) Ada language subset and to annotate the source code with additional information - at the benefit of being able to be complete (or sound) in the verification of certain properties, and without inundating the programmer with false alarms.
by Emma Adby

It's time to Make with Ada!
The challengeAre you ready to develop a project to the highest levels of safety, security and reliability? If so, Make with Ada is the challenge for you! We’re calling on embedded developers across the globe to build cool embedded applications using the Ada and SPARK programming languages and are offering over $8000 in total prizes. In addition, eligible students will compete for a reward of an Analog Discovery 2 Pro Bundle worth $299.99!
by Pamela Trevino
Public Ada Training Paris, France Dec 3 - 7, 2018
This course is geared to software professionals looking for a practical introduction to the Ada language with a focus on embedded systems, including real-time features as well as critical features introduced in Ada 2012. By attending this course you will understand and know how to use Ada for both sequential and concurrent applications, through a combination of live lectures from AdaCore's expert instructors and hands-on workshops using AdaCore's latest GNAT technology. AdaCore will provide an Ada 2012 tool-chain and ARM-based target boards for embedded workshops. No previous experience with Ada is required.
by Julia Teissl

Train control using Ada on a Raspberry Pi
I was looking for a topic for my master thesis in embedded systems engineering when one of my advisor proposed the idea of programming a control system for autonomous trains in Ada. Since I am fascinated by the idea of autonomous vehicles I agreed immediately without knowing Ada.
by Fabien Chouteau

Ada on FPGAs with PicoRV32
When I bought the TinyFPGA-BX board, I thought it would be an opportunity to play a little bit with FPGA, learn some Verilog or VHDL. But when I discovered that it was possible to have a RISC-V CPU on it, I knew I had to run Ada code on it.by Pamela Trevino
AdaCore major sponsor at HIS 2018
We are happy to announce that, AdaCore, alongside Altran and Jaguar Land Rover will be major sponsors of the fifth edition of the renowned High Integrity Software Conference on the 6th November in Bristol!
by Fabien Chouteau , Emma Adby , Yannick Moy

Learn.adacore.com is here
We are very proud to announce the availability of our new Ada and SPARK learning platform learn.adacore.com, which will replace AdaCoreU(niversity) e-learning platform. Learn all about it in this blog post.by Emma Adby , Fabien Chouteau

GNAT Community 2018 is here!
Calling all members of the Ada and SPARK community, we are pleased to announce that GNAT Community 2018 is here! adacore.com/download
by Yannick Moy
Security Agency Uses SPARK for Secure USB Key
ANSSI, the French national security agency, has published the results of their work since 2014 on designing and implementing an open-hardware & open-source USB key that provides defense-in-depth against vulnerabilities on the USB hardware, architecture, protocol and software stack. In this project called WooKey, Ada and SPARK are key components for the security of the platform. This is a very compelling demontration of both the usability and the power of safe languages and formal verification to develop secure systems.by Yannick Moy , Roderick Chapman

How Ada and SPARK Can Increase the Security of Your Software
There is a long-standing debate about which phase in the Software Development Life Cycle causes the most bugs: is it the specification phase or the coding phase? A recent study by NIST shows that, in the software industry at large, coding bugs are causing the majority of security issues. Choosing a safer language like Ada or SPARK is a critical component for reducing these vulnerabilities that result from simple mistakes. In a new freely available booklet, we explain how these languages and the associated toolsets can be used to increase the security of software.by Johannes Kanig
Taking on a Challenge in SPARK
Last week, the programmer Hillel posted a challenge (the link points to a partial postmortem of the provided solutions) on Twitter for someone to prove a correct implementation of three small programming problems: Leftpad, Unique, and Fulcrum.
by Thomas Quinot
PolyORB now lives on Github
PolyORB, AdaCore's versatile distribution middleware, now lives on Github. Its new home is https://github.com/AdaCore/polyorb
by Rob Tice

SPARKZumo Part 2: Integrating the Arduino Build Environment Into GPS
This is part #2 of the SPARKZumo series of blog posts. This post covers the build system that was used to build the SPARKZumo project and how to automate the process in GPS.by Fabien Chouteau , Yannick Moy , Vasiliy Fofanov , Nicolas Setton
A Modern Syntax for Ada
One of the most criticized aspect of the Ada language throughout the years has been its outdated syntax. Fortunately, AdaCore decided to tackle this issue by implementing a new, modern, syntax for Ada.by Fabien Chouteau

Getting Rid of Rust with Ada
There are a lot of DIY CNC projects out there (router, laser, 3D printer, egg drawing, etc.), but I never saw a DIY CNC sandblaster. So I decided to make my own.by Rob Tice
SPARKZumo Part 1: Ada and SPARK on Any Platform
So you want to use SPARK for your next microcontroller project? Great choice! All you need is an Ada 2012 ready compiler and the SPARK tools. But what happens when an Ada 2012 compiler isn’t available for your architecture?
by Yannick Moy

Two Days Dedicated to Sound Static Analysis for Security
AdaCore has been working with CEA, Inria and NIST to organize a two-days event dedicated to sound static analysis techniques and tools, and how they are used to increase the security of software-based systems. The program gathers top-notch experts in the field, from industry, government agencies and research institutes, around the three themes of analysis of legacy code, use in new developments and accountable software quality. Here is why it is worth attending.by Fabien Chouteau
Ada on the micro:bit
Updated July 2018
by Yannick Moy
Tokeneer Fully Verified with SPARK 2014
Tokeneer is a software for controlling physical access to a secure enclave by means of a fingerprint sensor. This software was created by Altran (Praxis at the time) in 2003 using the previous generation of SPARK language and tools, as part of a project commissioned by the NSA to investigate the rigorous development of critical software using formal methods. The project artefacts, including the source code, were released as open source in 2008. Tokeneer was widely recognized as a milestone in industrial formal verification. We recently transitioned this software to SPARK 2014, and it allowed us to go beyond what was possible with the previous SPARK technology. We have also shown how security vulnerabilities introduced in the code can be detected by formal verification.by Felix Krause
The Road to a Thick OpenGL Binding for Ada: Part 2
This blog post is part two of a tutorial based on the OpenGLAda project and will cover implementation details such as a type system for interfacing with C, error handling, memory management, and loading functions.by Yannick Moy

For All Properties, There Exists a Proof
With the recent addition of a Manual Proof capability in SPARK 18, it is worth looking at an example which cannot be proved by automatic provers, to see the options that are available for proving it with SPARK. We present three ways to complete a proof beyond what automatic provers can do: using an alternative automatic prover, proving interactively inside our GPS IDE, and using an alternative interactive prover.by Johannes Kanig

Bitcoin blockchain in Ada: Lady Ada meets Satoshi Nakamoto
Bitcoin is getting a lot of press recently, but let's be honest, that's mostly because a single bitcoin worth 800 USD in January 2017 was worth almost 20,000 USD in December 2017. However, bitcoin and its underlying blockchain are beautiful technologies that are worth a closer look. Let’s take that look with our Ada hat on!
by Felix Krause

The Road to a Thick OpenGL Binding for Ada: Part 1
This blog post is part one of a tutorial based on the OpenGLAda project and will cover some the background of the OpenGL API and the basic steps involved in importing platform-dependent C functions.
by Pierre-Marie de Rodat , Yannick Moy , Fabien Chouteau , Raphaël Amiard
AdaCore at FOSDEM 2018
Every year, free and open source enthusiasts gather at Brussels (Belgium) for two days of FLOSS-related conferences. FOSDEM organizers setup several “developer rooms”, which are venues that host talks on specific topics. This year, the event will happen on the 3rd and 4th of February (Saturday and Sunday) and there is a room dedicated to the Ada programming language.
by Lionel Matias
Leveraging Ada Run-Time Checks with Fuzz Testing in AFL
Fuzzing is a very popular bug finding method. The concept, very simple, is to continuously inject random (garbage) data as input of a software component, and wait for it to crash. If, like me, you find writing robustness test tedious and not very efficient in finding bugs, you might want to try fuzzing your Ada code.Here's a recipe to fuzz-test your Ada code, using American Fuzzy Lop and all the runtime checks your favorite Ada compiler can provide.Let's see (quickly) how AFL works, then jump right into fuzzing 3 open-source Ada libraries: ZipAda, AdaYaml, and GNATCOLL.JSON.by Pierre-Marie de Rodat , Raphaël Amiard
Cross-referencing Ada with Libadalang
Libadalang has come a long way since the last time we blogged about it. In the past 6 months, we have been working tirelessly on name resolution, a pretty complicated topic in Ada, and it is finally ready enough that we feel ready to blog about it, and encourage people to try it out.
by Manuel Iglesias Abbatermarco
Make with Ada 2017- Ada Based IoT Framework
SummaryThe Ada IoT Stack consists of an lwIp (“lightweight IP”) stack implementation written in Ada, with an associated high-level protocol to support embedded device connectivity nodes for today’s IoT world. The project was developed for the Make With Ada 2017 competition based on existing libraries and ported to embedded STM32 devices.
by Emma Adby
Welcoming New Members to the GNAT Pro Family
As we see the importance of software grow in applications, the quality of that software has become more and more important. Even outside the mission- and safety-critical arena customers are no longer accepting software failures (the famous blue screens of death, and there are many...). Ada has a very strong answer here and we are seeing more and more interest in using the language from a range of industries. It is for this reason that we have completed our product line by including an entry-level offer for C/C++ developers wanting to switch to Ada and reinforced our existing offer with GNAT Pro Assurance for programmers building the most robust software platforms with life cycles spanning decades.
by Fabien Chouteau
There's a mini-RTOS in my language
The first thing that struck me when I started to learn about the Ada programing language was the tasking support. In Ada, creating tasks, synchronizing them, sharing access to resources, are part of the language
by J. German Rivera

Make with Ada 2017- A "Swiss Army Knife" Watch
SummaryThe Hexiwear is an IoT wearable development board that has two NXP Kinetis microcontrollers. One is a K64F (Cortex-M4 core) for running the main embedded application software. The other one is a KW40 (Cortex M0+ core) for running a wireless connectivity stack (e.g., Bluetooth BLE or Thread). The Hexiwear board also has a rich set of peripherals, including OLED display, accelerometer, magnetometer, gryroscope, pressure sensor, temperature sensor and heart-rate sensor. This blog article describes the development of a "Swiss Army Knife" watch on the Hexiwear platform. It is a bare-metal embedded application developed 100% in Ada 2012, from the lowest level device drivers all the way up to the application-specific code, for the Hexiwear's K64F microcontroller. I developed Ada drivers for Hexiwear-specific peripherals from scratch, as they were not supported by AdaCore's Ada drivers library. Also, since I wanted to use the GNAT GPL 2017 Ada compiler but the GNAT GPL distribution did not include a port of the Ada Runtime for the Hexiwear board, I also had to port the GNAT GPL 2017 Ada runtime to the Hexiwear. All this application-independent code can be leveraged by anyone interested in developing Ada applications for the Hexiwear wearable device.
by 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 has been mostly solved for Ada in 2012 by our colleagues Ed Schonberg and Vincent Pucci who introduced special aspects for specifying physical dimensions on types. This dimension system did not attempt to deal with generics though. As was noted by others, handling generics in a dimensional analysis that is, like in GNAT, a compile-time analysis with no impact on the executable size or running time, is the source of the problem of dimension handling. Together with our partners from Technical Universitat München, we have finally solved this remaining difficulty.by 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 (BLDC/PMSM). It consist of a basic but clean and readable implementation of a sensored field oriented control algorithm. Included is a logging feature that will simplify development and allows users to visualize what is happening. The project shows that Ada successfully can be used for a bare-metal project that requires fast execution.by Pierre-Marie de Rodat

Highlighting Ada with Libadalang
While we are working very hard on semantic analysis in Libadalang, it is already possible to leverage its lexical and syntactic analyzers. A useful example for this is a syntax highlighter.
by Pierre-Marie de Rodat
Pretty-Printing Ada Containers with GDB Scripts
When things don’t work as expected, developers usually do one of two things: either add debug prints to their programs, or run their programs under a debugger. Today we’ll focus on the latter activity.
by 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 facilitate writing loop invariants by improving the documentation and the technology in different ways, but writing loops invariants remains difficult sometimes, in particular for beginners. To completely remove the need for loop invariants in simple cases, we have implemented loop unrolling in GNATprove. It turns out it is quite powerful when applicable.by 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 string search, and to find a previously unknown bug in a faster version of string search called quick search. Frama-C and SPARK share similar history, techniques and goals. So it was tempting to redo the same proofs on equivalent code in SPARK, and completing them with a functional proof of the fixed version of quick search. This is what I'll present in this post.by 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 focuses on a control algorithm and a simple serial communications protocol. The iRobot CreateⓇ 2 platform was originally design for STEM education and has great documentation and support - making it very easy to create a control application using Ada. This blog looks at the creation of the project and some cool features of Ada that were learned along the way.by Pierre-Marie de Rodat , Nicolas Setton

GNAT GPL 2017 is out!
For those users of the GNAT GPL edition, we are pleased to announce the availability of the 2017 release of GNAT GPL and SPARK GPL.
by Fabien Chouteau

Ada on the first RISC-V microcontroller
Updated July 2018
by Yannick Moy

Research Corner - Floating-Point Computations in SPARK
It is notoriously hard to prove properties of floating-point computations, including the simpler bounding properties that state safe bounds on the values taken by entities in the program. Thanks to the recent changes in SPARK 17, users can now benefit from much better provability for these programs, by combining the capabilities of different provers. For the harder cases, this requires using ghost code to state intermediate assertions proved by one of the provers, to be used by others. This work is described in an article which was accepted at VSTTE 2017 conference.by Yannick Moy
Frama-C & SPARK Day Slides and Highlights
The Frama-C & SPARK Day this week was a very successful event gathering the people interested in formal program verification for C programs (with Frama-C) and for Ada programs (with SPARK). Here is a summary of what was interesting for SPARK users. We also point to the slides of the presentations.by Yannick Moy
New Guidance for Adoption of SPARK
While SPARK has been used for years in companies like Altran UK, companies without the same know-how may find it intimidating to get started on formal program verification. To help with that process, AdaCore has collaborated with Thales throughout the year 2016 to produce a 70-pages detailed guidance document for the adoption of SPARK. These guidelines are based on five levels of assurance that can be achieved on software, in increasing order of costs and benefits: Stone level (valid SPARK), Bronze level (initialization and correct data flow), Silver level (absence of run-time errors), Gold level (proof of key properties) and Platinum level (full functional correctness). These levels, and their mapping to the Development Assurance Levels (DAL) and Safety Integrity Levels (SIL) used in certification standards, were presented at the recent High Confidence Software and Systems conference.by Fabien Chouteau

DIY Coffee Alarm Clock
A few weeks ago one of my colleagues shared this kickstarter project : The Barisieur. It’s an alarm clock coffee maker, promising to wake you up with a freshly brewed cup of coffee every morning. I jokingly said “just give me an espresso machine and I can do the same”. Soon after, the coffee machine is in my office. Now it is time to deliver :)by Yannick Moy
(Many) More Low Hanging Bugs
We reported in a previous post our initial experiments to create lightweight checkers for Ada source code, based on the new Libadalang technology. The two checkers we described discovered 12 issues in the codebase of the tools we develop at AdaCore. In this post, we are reporting on 6 more lightweight checkers, which have discovered 114 new issues in our codebase. This is definitely showing that these kind of checkers are worth integrating in static analysis tools, and we look forward to integrating these and more in our static analyzer CodePeer for Ada programs.by Yannick Moy , Nicolas Roche
A Usable Copy-Paste Detector in A Few Lines of Python
After we created lightweight checkers based on the recent Libadalang technology developed at AdaCore, a colleague gave us the challenge of creating a copy-paste detector based on Libadalang. It turned out to be both easier than anticipated, and much more efficient and effective than we could have hoped for. In the end, we hope to use this new detector to refactor the codebase of some of our tools, and we expect to integrate it in our IDEs.by Yannick Moy
VerifyThis Challenge in SPARK
This year again, the VerifyThis competition took place as part of ETAPS conferences. This is the occasion for builders and users of formal program verification platforms to use their favorite tools on common challenges. The first challenge this year was a good fit for SPARK, as it revolves around proving properties of an imperative sorting procedure. In this post, I am using this challenge to show how one can reach different levels of software assurance with SPARK.by Anthony Leonardo Gracio
GPS for bare-metal developers
In my previous blog article, I exposed some techniques that helped me rewrite the Crazyflie’s firmware from C into Ada and SPARK 2014, in order to improve its safety.
by Emmanuel Briot
User-friendly strings API
User friendly strings APIIn a previous post, we described the design of a new strings package, with improved performance compared to the standard Ada unbounded strings implementation. That post focused on various programming techniques used to make that package as fast as possible.
by Yannick Moy
GNATprove Tips and Tricks: Proving the Ghost Common Divisor (GCD)
Euclid's algorithm for computing the greatest common divisor of two numbers is one of the first ones we learn in school, and also one of the first algorithms that humans devised. So it's quite appealing to try to prove it with an automatic proving toolset like SPARK. It turns out that proving it automatically is not so easy, just like understanding why it works is not so easy. In this post, I am using ghost code to prove correct implementations of the GCD, starting from a naive linear search algorithm and ending with Euclid's algorithm.by Emmanuel Briot
New strings package in GNATCOLL
This post describes the new GNATCOLL.Strings package, and the various optimizations it performs to provide improved performance.by Jerome Guitton , Jérôme Lambourg , Joel Brobecker
Simics helps run 60 000 GNAT Pro tests in 24 hours
This post has been updated in March 2017 and was originally posted in March 2016.
by Pierre-Marie de Rodat
GNATcoverage moves to GitHub
Following the current trend, the GNATcoverage project moves to GitHub! Our new address is: https://github.com/AdaCore/gnatcoverage
by Jorge Real

Writing on Air
While searching for motivating projects for students of the Real-Time Systems course here at Universitat Politècnica de València, we found a curious device that produces a fascinating effect. It holds a 12 cm bar from its bottom and makes it swing, like an upside-down pendulum, at a frequency of nearly 9 Hz. The free end of the bar holds a row of eight LEDs. With careful and timely switching of those LEDs, and due to visual persistence, it creates the illusion of text... floating in the air!
by Fabien Chouteau , Arnaud Charlet , Yannick Moy
SPARK Tetris on the Arduboy
One of us got hooked on the promise of a credit-card-size programmable pocket game under the name of Arduboy and participated in its kickstarter in 2015. The kickstarter was successful (but late) and delivered the expected working board in mid 2016. Of course, the idea from the start was to program it in Ada , but this is an 8-bits AVR microcontroller (the ATmega32u4 by Atmel) not supported anymore by GNAT Pro. One solution would have been to rebuild our own GNAT compiler for 8-bit AVR from the GNAT FSF repository and use the AVR-Ada project. Another solution, which we explore in this blog post, is to use the SPARK-to-C compiler that we developed at AdaCore to turn our Ada code into C and then use the Arduino toolchain to compile for the Arduboy board.
by Emma Adby
AdaCore attends FOSDEM
Earlier this month AdaCore attended FOSDEM in Brussels, an event focused on the use of free and open source software. Two members of our technical team presented.by Pat Rogers
Getting started with the Ada Drivers Library device drivers
The Ada Drivers Library (ADL) is a collection of Ada device drivers and examples for ARM-based embedded targets. The library is maintained by AdaCore, with development originally (and predominantly) by AdaCore personnel but also by the Ada community at large. It is available on GitHub and is licensed for both proprietary and non-proprietary use.
by Raphaël Amiard , Yannick Moy , Pierre-Marie de Rodat
Going After the Low Hanging Bug
At AdaCore, we have a strong expertise in deep static analysis tools (CodePeer and SPARK), and we have been relying on the compiler GNAT and our coding standard checker GNATcheck to deal with more syntactic or weakly-semantic checks. The recent Libadalang technology, developed at AdaCore, provided us with an ideal basis to develop specialized light-weight static analyzers. As an experiment, we implemented two simple checkers using the Python binding of Libadalang. The results on our own codebase were eye-opening: we found a dozen bugs in the codebases of the tools we develop at AdaCore (including the compiler and static analyzers).by Raphaël Amiard , Pierre-Marie de Rodat
Introducing Libadalang
AdaCore is working on a host of tools that works on Ada code. The compiler, GNAT, is the most famous and prominent one, but it is far from being the only one. At AdaCore, we already have several other tools to process Ada code: the ASIS library, GNAT2XML, the GPS IDE. A realization of the past years, however, has been that we were lacking a unified solution to process code that is potentially evolving, potentially incorrect Ada code. Hence Libadalang.by Yannick Moy
New Year's Resolution for 2017: Use SPARK, Say Goodbye to Bugs
NIST has recently published a report called "Dramatically Reducing Software Vulnerabilities" in which they single out five approaches which have the potential for creating software with 100 times fewer vulnerabilities than we do today. One of these approaches is formal methods. Among formal methods, the report highlights strong suits of SPARK, and cites SPARK projects as example of mature uses of formal methods. NIST is not the only ones to support the use of SPARK. Editor Bill Wong from Electronic Design has included SPARK in his "2016 Gifts for the Techie". So if your new year's resolutions include software without bugs, have a look at SPARK in 2017.by Johannes Kanig
SPARK and CodePeer, a Good Match!
It turns out that the CodePeer engine can be used as a powerful prover for SPARK programs. This feature will be available in the next version of SPARK Pro, make sure you try it out!by Fabien Chouteau
Make with Ada: DIY instant camera
There are moments in life where you find yourself with an AdaFruit thermal printer in one hand, and an OpenMV camera in the other.by Emma Adby
Building High-Assurance Software without Breaking the Bank
AdaCore will be hosting a joint webcast next Monday 12th December 2pm ET/11am PT with SPARK experts Yannick Moy and Rod Chapman. Together, they will present the current status of the SPARK solution and explain how it can be successfully adopted in your current software development processes.
by Emma Adby
Make With Ada Winners Announced!
Judging for the first annual Make with Ada competition has come to an end and we can now reveal the results.
by Sylvain Dailler
GNATprove Tips and Tricks: a Lemma for Sorted Arrays
We report on the creation of the first lemma of a new lemma library on arrays: a lemma on transitivity of the order in arrays.by Claire Dross
Automatic Generation of Frame Conditions for Array Components
One of the most important challenges for SPARK users is to come up with adequate contracts and annotations, allowing GNATprove to verify the expected properties in a modular way. Among the annotations mandated by the SPARK toolset, the hardest to come up with are probably loop invariants. A previous post explains how GNATprove can automatically infer loop invariants for preservation of unmodified record components, and so, even if the record is itself nested inside a record or an array. Recently, this generation was improved to also support the simplest cases of partial array updates. We describe in this post in which cases GNATprove can, or cannot, infer loop invariants for preservation of unmodified array components.by Yannick Moy
GNATprove Tips and Tricks: What’s Provable for Real Now?
One year ago, we presented on this blog what was provable about fixed-point and floating-point computations (the two forms of real types in SPARK). Since then, we have integrated static analysis in SPARK, and modified completely the way floating-point numbers are seen by SMT provers. Both of these features lead to dramatic changes in provability for code doing fixed-point and floating-point computations.by Emmanuel Briot

Integrate new tools in GPS
This blog, the first in a series, explains the basic mechanisms that GPS (the GNAT Programming Studio) provides to integrate external tools. A small plugin might make your daily workflow more convenient by providing toolbar buttons and menus to spawn your tool and parse its output.by Pat Rogers

Driving a 3D Lunar Lander Model with ARM and Ada
One of the interesting aspects of developing software for a bare-board target is that displaying complex application-created information typically requires more than the target board can handle. Although some boards do have amazing graphics capabilities, in some cases you need to have the application on the target interact with applications on the host. This can be due to the existence of special applications that run only (or already) on the host, in particular.
by Yannick Moy
Research Corner - SPARK on Lunar IceCube Micro Satellite
Researchers Carl Brandon and Peter Chapin recently presented during conference HILT 2016 their ongoing work to build a micro satellite called Lunar IceCube that will map water vapor and ice on the moon. In their paper, they explain how the use of proof with SPARK is going to help them get perfect software in the time and budget available.by Piotr Trojanek
Verifying Tasking in Extended, Relaxed Style
Tasking was one of the big features introduced in the previous release of SPARK 2014. However, GNATprove only supported tasking-related constructs allowed by the Ravenscar profile. Now it also supports the more relaxed GNAT Extended Ravenscar profile.by Olivier Ramonat
Simplifying our product versioning
Looking at the list of product versions that were expected for 2017 it became clear that we had to review the way we were handling product versioning.by Claire Dross
SPARK 2014 Rationale: Support for Type Invariants
Type invariants are used to model properties that should always hold for users of a data type but can be broken inside the data type implementation. Type invariant are part of Ada 2012 but were not supported in SPARK until SPARK Pro 17.by Yannick Moy
Verified, Trustworthy Code with SPARK and Frama-C
Last week, a few of us at AdaCore have attended a one-day workshop organized at Thales Research and Technologies, around the topic of "Verified, trustworthy code - formal verification of software". Attendees from many different branches of Thales (avionics, railway, security, networks) were given an overview of the state-of-practice in formal verification of software, focused on two technologies: the SPARK technology that we develop at AdaCore for programs in Ada, and the Frama-C technology developed at CEA research labs for programs in C. The most interesting part of the day was the feedback given by three operational teams who have experimented during a few months with either SPARK (two teams) or Frama-C (one team). The lessons learned by first-time adopters of such technologies are quite valuable.by Yannick Moy
The Most Obscure Arithmetic Run-Time Error Contest
Something that many developers do not realize is the number of run-time checks that occur in innocent looking arithmetic expressions. Of course, everyone knows about overflow checks and range checks (although many people confuse them) and division by zero. After all, these are typical errors that do show up in programs, so programmers are aware that they should keep an eye on these. Or do they?by Quentin Ochem

Unity & Ada
Using Ada technologies to develop video games doesn’t sound like an an obvious choice - although it seems like there could be an argument to be made. The reverse, however, opens some more straightforward perspectives.by Emmanuel Briot

GNAT Programming Studio (GPS) on GitHub
The GPS source repository has been published on GitHub. This post briefly describes how you can access it, and hopefully contribute.by Claire Dross
Automatic Generation of Frame Conditions for Record Components
Formal verification tools like GNATprove rely on the user to provide loop invariants to describe the actions performed inside loops. Though the preservation of variables which are not modified in the loop need not be mentioned in the invariant, it is in general necessary to state explicitly the preservation of unmodified object parts, such as record fields or array elements. These preservation properties form the loop’s frame condition. As it may seem obvious to the user, the frame condition is unfortunately often forgotten when writing a loop invariant, leading to unprovable checks. To alleviate this problem, the GNATprove tool now generates automatically frame conditions for preserved record components. In this post, we describe this new feature on an example.by Emma Adby

Introducing the Make With Ada competition!
If you’ve been looking for a way to start your next embedded project in Ada or SPARK. Then, look no further than the Make with Ada competition!
by Yannick Moy
Research Corner - Proving Security of Binary Programs with SPARK
Researchers from Dependable Computing and Zephyr Software LLC have presented at the latest NASA Formal Methods conference last week their work on proving security of binary programs. In this work, they use SPARK as intermediate language and GNATprove as proof tool, which is an atypical and interesting use of the SPARK technology.by Pierre-Marie de Rodat

C library bindings: GCC plugins to the rescue
I recently started working on an Ada binding for the excellent libuv C library. This library provides a convenient API to perform asynchronous I/O under an event loop, which is a popular way to develop server stacks. A central part of this API is its enumeration type for error codes: most functions use it. Hence, one of the first things I had to do was to bind the enumeration type for error codes. Believe it or not: this is harder than it first seems!
by Fabien Chouteau

Make with Ada: ARM Cortex-M CNC controller
I started this project more than a year ago. It was supposed to be the first Make with Ada project but it became the most challenging from both, the hardware and software side.
by Yannick Moy

GNATprove Tips and Tricks: Using the Lemma Library
A well-know result of computing theory is that the theory of arithmetic is undecidable. This has practical consequences in automatic proof of programs which manipulate numbers. The provers that we use in SPARK have a good support for addition and subtraction, but much weaker support for multiplication and division. This means that as soon as the program has multiplications and divisions, it is likely that some checks won't be proved automatically. Until recently, the only way forward was either to complete the proof using an interactive prover (like Coq or Isabelle/HOL) or to justify manually the message about an unproved check. There is now a better way to prove automatically such checks, using the recent SPARK lemma library.by Claire Dross
Quantifying over Elements of a Container
Containers holding several items of the same type such as arrays, lists, or sets are a common occurrence in computer programs. Stating a property over such containers often involves quantifying over the elements they contain. The way quantified formulas over containers are translated for proof can be tuned in GNATprove using a specific annotation.by Florian Schanda
SPARKSMT - An SMTLIB Processing Tool Written in SPARK - Part I
Today I will write the first article in a short series about the development of an SMTLIB processing tool in SPARK. Instead of focusing on features, I intend to focus on the how I have proved absence of run-time errors in the name table and lexer. I had two objectives: show absence of run-time errors, and do not write useless defensive code. Today's blog will be about the name table, a data structure found in many compilers that can map strings to a unique integer and back. The next blog post will talk about the lexical analyzer.by Emma Adby
Certification and Qualification
AdaCore provides several tools with certification and qualification capabilities, for the rail and avionics industry. Quentin Ochem’s presentation on “Certification and Qualification” at the 2015 AdaCore Tech Days in Boston, Massachusetts provided more information about these two standards, namely DO-178C and EN:50128:2011.
by Jérôme Lambourg
Efficient use of Simics for testing
As seen in the previous blog article, AdaCore relies heavily on virtualisation to perform the testing of its GNAT Pro products for VxWorks.
by Emma Adby

VectorCAST/Ada: Ada 2012 Language Support
We are pleased to announce that on April 27th our partner, Vector, will host a webinar to showcase their latest VectorCAST/Ada release!
by Emma Adby

Provably safe programming at Embedded World
AdaCore continues to build reliable and secure software for embedded software development tools. Last month, we attended Embedded World 2016, one of the largest conferences of its kind in Europe, to present our embedded solutions and our expertise for safety, and mission critical applications in a variety of domains.
by Emma Adby

CubeSat continues to orbit the Earth thanks to Ada & SPARK!
Dr Carl Brandon of Vermont Technical College and his team of students used SPARK and Ada to successfully launch a satellite into space in 2013 and it has continued to orbit the Earth ever since! At our AdaCore Tech Days in Boston last year Dr Brandon explained further.
by Yannick Moy
Formal Verification of Legacy Code
Just a few weeks ago, one of our partners reported a strange behavior of the well-known function Ada.Text_IO.Get_Line, which reads a line of text from an input file. When the last line of the file was of a specific length like 499 or 500 or 1000, and not terminated with a newline character, then Get_Line raised an exception End_Error instead of returning the expected string. That was puzzling for a central piece of code known to have worked for the past 10 years! But fair enough, there was indeed a bug in the interaction between subprograms in this code, in boundary cases having to do with the size of an intermediate buffer. My colleague Ed Schonberg who fixed the code of Get_Line had nonetheless the intuition that this particular event, finding such a bug in an otherwise trusted legacy piece of code, deserved a more in depth investigation to ensure no other bugs were hiding. So he challenged the SPARK team at AdaCore in checking the correctness of the patched version. He did well, as in the process we uncovered 3 more bugs.
by Fabien Chouteau

Make with Ada: Candy dispenser, with a twist...
A few months ago, my colleague Rebecca installed a candy dispenser in our kitchen here at AdaCore. I don’t remember how exactly, but I was challenged to make it more… fun.
by Emma Adby

Embedded Product Line Updates
Embedded products are not stand alone, this allows them to have safety, mission critical and real-time requirements that they wouldn’t necessarily have otherwise. The embedded product line provides analyzable, verifiable, and certifiable software for both static and dynamic analysis tools.
by Emma Adby

QGen 2.1 Release!
Embedded World will see the latest release of QGen, the qualifiable and customisable code generator for Simulink® and Stateflow® models!
by Emma Adby
Formal Verification Made Easy!
We are pleased to announce our latest release of SPARK Pro! A product that has been jointly developed alongside our partner Altran and following the global AdaCore Tech Days, you can now see the SPARK 2014 talk, Formal Verification Made Easy by AdaCore’s Hristian Kirtchev, on YouTube.
by Emma Adby

ERTS and Embedded World conferences 2016
We are pleased to announce that we will be a major sponsor and exhibitor at ERTS, Toulouse and will be exhibiting at Embedded World, Nuremberg in the coming months!
by Jérôme Lambourg

Porting the Ada Runtime to a new ARM board
A step by step tutorial to adapt the ARM runtime to new MCUs/boards.by Yannick Moy , Emma Adby

Ada Lovelace Bicentennial
The three of us attended the Ada Lovelace Symposium in Oxford (UK). The two days were one fantastic discovery after another about the life, achievements and legacy of Ada Lovelace, the programming pioneer who lent her name to the Ada language.
by Emma Adby
Dissimilar tools: Use cases and impact on tool qualification level
Frederick Pothon of ACG Solutions has recently published a document entitled - Dissimilar tools: Use cases and impact on tool qualification level on the open-DO blog.
by Yannick Moy
GNATprove Tips and Tricks: What’s Provable for Real?
SPARK supports two ways of encoding reals in a program: the usual floating-point reals, following the standard IEEE 754, and the lesser known fixed-point reals, called this way because their precision is fixed (contrary to floating-points whose precision varies with the magnitude of the encoded number). This support is limited in some ways when it comes to proving properties of computations on real numbers, and these limitations depend strongly in the encoding chosen. In this post, I show the results of applying GNATprove on simple programs using either floating-point or fixed-point reals, to explain these differences.by Yannick Moy
SPARK 2014 Rationale: Support for Ravenscar
As presented in a recent post by Pavlos, the upcoming release of SPARK Pro will support concurrency features of Ada, with the restrictions defined in the Ravenscar profile of Ada. This profile restricts concurrency so that concurrent programs are deterministic and schedulable. SPARK analysis makes it possible to prove that shared data is protected against data races, that deadlocks cannot occur and that no other run-time errors related to concurrency can be encountered when running the program. In this post, I revisit the example given by Pavlos to show SPARK features and GNATprove analysis in action.by Emmanuel Briot
Calling inherited subprograms in Ada
This short post describes an idiom that can be used to help maintain complex hierarchies of tagged types, when methods need to call the parent types methods.by Florian Schanda
SPARK 2016 Supports Ravenscar!
The new big feature of the SPARK 2016 release is the support of the Ravenscar profile. Users can now use protected objects and tasks to write concurrent code. On uniprocessor computers the toolset can ensure that no deadlocks or data races will occur and that no tasks will terminate. Read this blog post to learn more and see the new feature in practice.by Fabien Chouteau
Make with Ada: Formal proof on my wrist
When the Pebble Time kickstarter went through the roof, I looked at the specification and noticed the watch was running on an STM32F4, an ARM cortex-M4 CPU which is supported by GNAT. So I backed the campaign, first to be part of the cool kids and also to try some Ada hacking on the device.by Emma Adby

Modernizing Adacore's Open-Source Involvement
Through the adoption of GitHub we have taken our first step on the way to having a more collaborative and dynamic interaction with, both our users and open source technologies.
by David Hauzar

SPARK 16: Generating Counterexamples for Failed Proofs
While the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would automatically find values of variables showing why a proof fails. SPARK Pro 16, to be released in 2016, is going to introduce such a feature. If a proof fails, it attempts to generate a counterexample exhibiting the problem. This post introduces this new feature, developed in the scope of the ProofInUse laboratory.by Emma Adby
ARM TechCon and NBAA Conference 2015
We are continuing to develop tools for use within projects that require reliable and secure embedded software for ARM. Our engineering team have been busy creating demos running on ARM technology, such as Tetris in SPARK on ARM Cortex M4.
by Maxim Reznik , Nicolas Setton
Using reference types to handle persistent objects
The Ada 2012 standard introduced user-defined references. The main idea behind this is simplifying the access to elements in a container. But you can use them to control the life-circle of your persistent objects. Let's see how it could work.
by Emma Adby

HIS Conference 2015, Bristol
We are excited to be sponsoring and exhibiting at the 2nd annual High Integrity Software conference, taking place on 5th November 2015 at The Royal Marriott Hotel in Bristol.
by Emma Adby

AdaCore Tech Days 2015
by Florian Schanda
SPARK 2014 Rationale: Variables That Are Constant
The SPARK tools now support yet another feature that allows users to better specify the intended behavior of their programs. This new feature enables users to declare that specific variables can only be updated during the elaboration of their enclosing package. Read on if you want to know more...by Emmanuel Briot
Traits-Based Containers
This post describes the design of a new containers library. It highlights some of the limitations of the standard Ada containers, and proposes a new approach using generic packages as formal parameters to make these new containers highly configurable at compile time.by Yannick Moy
New Book About SPARK 2014
I am very pleased to announce that a book is now available for those who want to learn formal verification with SPARK 2014. This book was written by Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College. We've been interacting a lot with them since they started in 2013, and the result of these interactions is quite satisfying!by Raphaël Amiard

Make with Ada : From bits to music
I started out as an electronic musician, so one of my original motivations when I learnt programming was so that I could eventually *program* the sounds I wanted rather than just use already existing software to do it.
by Jack Mellor
2015: A Space Ada‑ssey
AdaCore has a long history of providing tools and support to develop mission critical applications for Space. Check out this video we made and showed at the conference to see which ones!by Yannick Moy
SPARK 2014 Rationale: Type Predicates
Preconditions and postconditions define a very strong mechanism for specifying invariant properties over the program's control. What about similar properties for the program's data? It turns out Ada 2012 defined such a construct, type predicates, which was not supported in SPARK until now. And now it is.by Fabien Chouteau

Make with Ada: "The Eagle has landed"
July 20, 1969, 8:18 p.m. UTC, while a bunch of guys were about to turn blue on Earth, commander Neil A. Armstrong confirms the landing of his Lunar Module (LM), code name Eagle, on the moon. Will you be able to manually land Eagle on the Sea of Tranquillity?by Cyrille Comar

Farewell Robert...
It is with great sadness that I have to announce the death of Robert Dewar...
by Fabien Chouteau

Make with Ada: All that is useless is essential
A few weeks ago I discovered the wonderful world of solenoid engines. The idea is simple: take a piston engine and replace explosion with electromagnetic field. In this article I will experiment a solenoid engine using a hacked hard drive and a software controller on a STM32F4 .by Anthony Leonardo Gracio
How to prevent drone crashes using SPARK
The Crazyflie is a very small quadcopter sold as an open source development platform: both electronic schematics and source code are directly available on their GitHub and its architecture is very flexible. Even if the Crazyflie flies out of the box, it has not been developed with safety in mind: in case of crash, its size, its weight and its plastic propellers won’t hurt anyone! But what if the propellers were made of carbon fiber, and shaped like razor blades to increase the drone’s performance? In theses circumstances, a bug in the flight control system could lead to dramatic events. In this post, I present the work I did to rewrite the stabilization system of the Crazyflie in SPARK 2014, and to prove that it is free of runtime errors. SPARK also helped me to discover little bugs in the original firmware, one of which directly related with overflows. Besides the Crazyflie, this work could be an inspiration for others to do the same work on larger and more safety-critical drones.by Yannick Moy
How Our Compiler Learnt From Our Analyzers
Program analyzers interpret the source code of a program to compute some information. Hopefully, the way they interpret the program is consistent with the way that the compiler interprets it to generate an executable, or the information computed is irrelevant, possibly misleading. For example, if the analyzer says that there are no possible run-time errors in a program, and you rely on this information to compile with dynamic checking off, it is crucial that no run-time error could occur as a result of a divergence of opinion between the analyzer and the compiler on the meaning of an instruction. We recently discovered such an inconsistency in how our compiler and analyzers dealt with floating-point exponentiation, which lead to a change in how GNAT now compile these operations.by Emmanuel Briot
Count them all (reference counting)
Reference countingReference counting is a way to automatically reclaim unused memory. An element is automatically deallocated as soon as there are no more references to it in the program.
by Emmanuel Briot
Larger than it looks (storage pools)
This post shows how to implement a special storage pool that allocates an extra header every time it allocates some memory. This can be used to store type specific information, outside of the type itself.by Karen Mason

What's in the Box?
Forget about the black box - we want you to see what's in the AdaCore box! Our machine room, the life blood of the company, is centered in the office space in a glass box and is pure eye candy for geeks and cable aficionados. The machine room is 204 sq ft (19 sq meters), contains 73 machines (running the gamut from VxWorks, Linux, Windows, Android and more) 1.5 miles of cables and a state of the art fire suppression mechanism! Oh and the modern air intake system gives it a green energy seal of approval. In the unlikely event of a fire; the smoke detectors allow 30 seconds before dispersing an agent called FM200 which will suppress the fire but not damage the equipment. The economizer takes advantage of winters' freeze and draws cool air from the outside to cool the machine room and the heated air is then spilled to common office areas thus reducing heating costs. We're proud to show-off the hardware side of our software!
by Emma Adby

Project P Open Workshop
Project-P Open Workshop
by Emma Adby
Verification on Ada code with Static and Dynamic Code Analysis - Webinar
One of the main challenges to get certification in Ada projects is the achievement of 100% code coverage but in most projects an amount of more than 95% structural coverage is hard to achieve. What can you do with the last 5% of code that can't be covered? DO-178C for example, provides a framework for the integration of various techniques in the development process to solve the problem. In this webinar you learn how static analysis and dynamic testing can help complete analysis for pieces of code that are not covered.
by Karen Mason

The Year for #AdaLove
Despite her famously sharp analytical mind, it’s unlikely Ada Lovelace could have predicted the durability of her legacy as the world’s first computer programmer and pioneer for women in computing.
by Claire Dross
A quick glimpse at the translation of Ada integer types in GNATprove
In SPARK, as in most programming languages, there are a bunch of bounded integer types. On the other hand, Why3 only has mathematical integers and a library for bitvectors. Since bitwise operations can only be done on modular types in Ada, we currently translate arithmetic operations on signed integer types as operations on mathematical integers and arithmetic operations on modular types as operation on bitvectors. The only remaining question now is, how do we encode specific bounds of the Ada types into our Why3 translation ? In this post, I will present three different ways we tried to do this and explain which one we currently use and why.by Martyn Pike
The latest Mixed Programming with Ada lectures at the AdaCore University
I recently joined AdaCore as a Technical Account Manager with an initial focus on the UK and Scandinavian regions, but for the last 12 months I've been busy working on the AdaCore University. The most recent addition to which is a course on Mixed Language Programming with Ada, and it includes lectures on the integration of Ada with C, C++ and Java. The course covers some advanced topics like mixed language object orientation, techniques for using Ada strong typing to combat known issue with C pointers and the pitfalls that are encountered when mixing native Ada code with Java at runtime. This course clearly demonstrates that Ada has strong support for integration with C, C++ and Java and it proves there are no technical barriers to its adoption in modern mixed language software systems.
by Yannick Moy

A Building Code for Building Code
In a recent article in Communications of the ACM, Carl Landwehr, a renowned scientific expert on security, defends the view that the software engineering community is doing overall a poor job at securing our global information system and that this is mostly avoidable by putting what we know works to work, to the point that most vulnerabilities could be completely avoided by design if we cared enough. Shocking! Or so it should appear.by Clément Fumex
GNATprove Tips and Tricks: Bitwise Operations
The ProofInUse joint laboratory is currently improving the way SPARK deals with modular types and bitwise operators. Until now the SPARK tool was trying its best to translate those into equivalent operations on integers. It is now using native theory of smt-solvers when available resulting in much better support, and guaranteeing state of the art handling of bitwise operations. We present some examples in this post.by Emma Adby

20 years on...
20 Years of AdaCore: Company as Committed as Ever on Safety-Critical Software Solutions
by Olivier Ramonat

AdaCore Releases GNAT Pro 7.3, QGen 1.0 and GNATdashboard 1.0
February saw the annual customer release of a number of important products. This is no mean task when you consider the fact that GNAT Pro is available on over 50 platforms and supports over 150 runtime profiles (ranging from Full Ada Support to the very restricted Zero Footprint Profile suitable for safety-critical development). All in all, from the branching of the preview version to the customer release it takes us nearly 4 months to package everything up! Quality is assured through the internally developed AdaCore Factory.
by Johannes Kanig
Testing, Static Analysis, and Formal Verification
I've recently written an article (in two parts) over at Electronic Design about applying different methods of verification to the same small piece of code. The code in question is an implementation of binary search, and I applied Testing, Static Analysis (using the AdaCore tool CodePeer) and Formal Verification (using the AdaCore tool SPARK 2014).
by Yannick Moy
AdaCore Tech Days Prez on SPARK
Hristian Kirtchev, who leads the developments of the GNAT compiler frontend, gave a very clear presentation of SPARK at the last AdaCore Tech Days in Boston. This was recorded, here is the video.
by Yannick Moy
GNATprove Tips and Tricks: Catching Mistakes in Contracts
Contracts may be quite complex, as complex as code in fact, so it is not surprising that they contain errors sometimes. GNATprove can help by pinpointing suspicious constructs that, although legal, do not make much sense. These constructs are likely to be caused by mistakes made by the programmer when writing the contract. In this post, I show examples of incorrect constructs that are signaled by GNATprove.by Tristan Gingold
AdaCore at FOSDEM'15
I was at Bruxelles on January 31st to present the components of GNAT GPL 2015 : SPARK 2014 and GNAT GPL for ARM bare-board. This is not unrelated to a previous blog entry on Tetris in SPARK on ARM Cortex M4, in particular I presented that Tetris demo (I brought some boards with me and despite the simple package, none were broken!). The slides contain technical details on the ravenscar profile (main principles), how to build a program for the stm32f4-discovery board and how to port the runtime. There are also less technical slides such as why we choose the stm32f4 board and photos of some graphical demos. As that could be useful to anyone interested in Ravenscar or in porting the runtime to other boards or other platforms, we've made the slides available here.
by Lena Comar

ProofInUse is coming!
For lovers of verification tools and critical system (we know you're out there!), we are very excited to present ProofInUse!
by Yannick Moy
SPARK 2014 Rationale: Functional Update
While attribute Old allows expressing inside postconditions the value of objects at subprogram entry, this is in general not enough to conveniently express how record and array objects are modified by a procedure. A special attribute Update is defined in SPARK to make it easy to express such properties.by Emma Adby

A Busy Schedule Ahead!
If you have a passion for Ada, need more information on our technology or would just like to have a chat, there are a couple of upcoming events where we'd love to meet up. What's more, we'll be launching our brand new product QGen at Embedded World!
by Yannick Moy
SPARK 2014 Rationale: Object Oriented Programming
Object Oriented Programming is known for making it particularly difficult to analyze programs, because the subprograms called are not always known statically. The standard for civil avionics certification has recognized this specific problem, and defines a specific verification objective called Local Type Consistency that should be met with one of three strategies. SPARK allows using one of these strategies, by defining the behavior of an overridden subprogram using a special class-wide contract and checking that the behavior of the overriding subprogram is a suitable substitution, following the Liskov Substitution Principle.by Tristan Gingold , Yannick Moy

Tetris in SPARK on ARM Cortex M4
Tetris is a well-known game from the 80's, which has been ported in many versions to all game platforms since then. There are even versions of Tetris written in Ada. But there was no version of Tetris written in SPARK, so we've repaired that injustice. Also, there was no version of Tetris for the Atmel SAM4S ARM processor, another injustice we've repaired.
by Cyrille Comar
Welcome To AdaCore's Blog
I'm proud, if not a bit nervous, to be the one firing the very first post on this brand new blog. Why are we starting a corporate blog at this time? There are many reasons for this. The main one is that there are many things happening at AdaCore and around the GNAT technology and we are seeking better ways to make them widely known while offering interested recipients the possibility to react and interact with us.by Yannick Moy
SPARK 2014 Rationale: Ghost Code
A common situation when proving properties about a program is that you end up writing additional code whose only purpose is to help proving the original program. If you're careful or lucky enough, the additional code you write will not impact the program being verified, and it will be removed during compilation, so that it does not inflate binary size or waste execution cycles. SPARK provides a way to get these benefits automatically, by marking the corresponding code as ghost code, using the new Ghost aspect.by Yannick Moy

Using SPARK to Prove AoRTE in Robot Navigation Software
Correctness of robot software is a challenge. Just proving the absence of run-time errors (AoRTE) in robot software is a challenge big enough that even NASA has not solved it. Researchers have used SPARK to do precisely that for 3 well-known robot navigation algorithms. Their results will be presented at the major robotics conference IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS 2014) this coming September.by Johannes Kanig

Explicit Assumptions in SPARK 2014
In this article, we provide a short introduction to our paper at the Test and Proof 2014 conference in York, UK.by Claire Dross
External Axiomatizations: a Trip Into SPARK’s Internals
There are cases expressing all the specification of a package in SPARK is either impossible (for example if you need to link them to elements of the mathematical world, like trigonometry functions), cumbersome (especially if they require concepts that cannot easily be described using contracts, like transitivity, counting, summation...), or simply inefficient, for big and complex data structures like containers for example. In these cases, a user can provide directly a manually written Why3 translation for an Ada package using a feature named external axiomatizations. Coming up with this manual translation requires both a knowledge of the WhyML language and a minimal understanding of GNATprove's mechanisms and is therefore reserved to advanced users.by Claire Dross
Manual Proof with Ghost Code in SPARK 2014
Guiding automatic solvers by adding intermediate assertions is a commonly used technique. We can go further in this direction, by adding complete pieces of code doing nothing, generally called ghost code, to guide the automated reasoning. This is an advanced feature, for people willing to manually guide proofs. Still, it is all in SPARK 2014 and thus does not require the user to learn a new language. We explain here how we can achieve inductive proofs on a permutation function.by Claire Dross
Contracts of Functions in SPARK 2014
In SPARK 2014, we can write a function F and annotate it with a pre and a postcondition. In this post, we explain how the SPARK 2014 proof tool handles a call to such a function.by Florian Schanda
SPARK 2014 Rationale: Information Flow
In a previous blog post we described how aspect Global can be used to designate the specific global variables that a subprogram has to read and write. So, by reading the specification of a subprogram that has been annotated with aspect Global we can see exactly which variables, both local and global, are read and/or written each time the subprogram is called. Based purely on the Global aspect, this pretty much summarizes the full extent of our knowledge about the flow of information in a subprogram. To be more precise, at this point, we know NOTHING about the interplay between the inputs and outputs of the subprogram. For all we know, all outputs could be randomly generated and the inputs might not contribute in the calculation of any of the outputs. To improve this situation, SPARK 2014 uses aspect Depends to capture the dependencies between a subprogram's outputs and inputs. This blog post demonstrates through some examples how aspect Depends can be used to facilitate correct flow of information through a subprogram.by Johannes Kanig
Prove in Parallel with SPARK 2014
The article explains how we improved the performance of the SPARK 2014 toolset when multiple CPU cores are available for proof.by Yannick Moy
