165 entries tagged with #OSS
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 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 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 Yannick Moy
SPARKNaCl - Two Years of Optimizing Crypto Code in SPARK (and counting)
SPARKNaCl is a SPARK version of the TweetNaCl cryptographic library, developed by formal methods and security expert Rod Chapman. For two years now, Rod has been developing and optimizing this open-source cryptographic library while preserving the automatic type-safety proof across code changes and tool updates. He has recently given a talk about this experience that I highly recommend.
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 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 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 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 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: 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 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 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 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

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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 Yannick Moy
Secure Software Architectures Based on Genode + SPARK
SPARK user Alexander Senier presented recently at BOB Konferenz in Germany their use of SPARK for building secure mobile architectures. What's nice is that they build on the guarantees that SPARK provides at software level to create a secure software architecture based on the Genode operating system framework. They present 3 interesting architectural designs that make it possible to build a trustworthy system out of untrustworthy building blocks. Almost as exciting as Alchemy's goal of transforming lead into gold! Here is the video of that presentation.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 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 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 Fabien Chouteau

Ada on the first RISC-V microcontroller
Updated July 2018
by Yannick Moy
Research Corner - FLOSS Glider Software in SPARK
Two years ago, we redeveloped the code of a small quadcopter called Crazyflie in SPARK, as a proof-of-concept to show it was possible to prove absence of run-time errors (no buffer overflows, not division by zero, etc.) on such code. The researchers Martin Becker and Emanuel Regnath have raised the bar by developing the code for the autopilot of a small glider in SPARK in three months only. Their paper and slides are available, and they have released their code as FLOSS for others to use/modify/enhance!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 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 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 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 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 Johannes Kanig
Hash it and Cache it
A new feature of SPARK2014 allows to use a memcached server to share proof results between runs of the SPARK tools and even between developers on different machines. Check out this post to see the details.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 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 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 Emmanuel Briot

Debugger improvements in GPS 17
The GNAT Programming Studio support for the debugger has been enhanced. This post describes the various changes you can expect in this year's new release of GPS.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 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 Yannick Moy
Did SPARK 2014 Rethink Formal Methods?
David Parnas is a well-known researcher in formal methods, who famously contributed to the analysis of the shut-down software for the Darlington nuclear power plant and designed the specification method known as Parnas tables and the development method called Software Cost Reduction. In 2010, the magazine CACM asked him to identify what was preventing more widespread adoption of formal methods in industry, and in this article on Really Rethinking Formal Methods he listed 17 areas that needed rethinking. The same year, we started a project to recreate SPARK with new ideas and new technology, which lead to SPARK 2014 as it is today. Parnas's article influenced some critical design decisions. Six years later, it's interesting to see how the choices we made in SPARK 2014 address (or not) Parnas's concerns.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 AdaCore Admin
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 Yannick Moy , Jamie Ayre , 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 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 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 AdaCore Admin

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 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 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 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 Yannick Moy
SPARKSkein: From tour-de-force to run-of-the-mill Formal Verification
In 2010, Rod Chapman released an implementation in SPARK of the Skein cryptographic hash algorithm, and he proved that this implementation was free of run-time errors. That was a substantial effort with the previous version of the SPARK technology. We have recently translated the code of SPARKSkein from SPARK 2005 to SPARK 2014, and used GNATprove to prove absence of run-time errors in the translated program. The difference between the two technologies is striking. The heroic effort that Rod put in the formal verification of the initial version of SPARKSkein could now be duplicated with modest effort and modest knowledge of the technology, thanks to the much greater proof automation that the SPARK 2014 technology provides, as well as various features that lower the need to provide supporting specifications, most notably contracts on internal subprograms and loop invariants.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 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 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 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 Yannick Moy
GNATprove Tips and Tricks: Keeping Justifications Up-To-Date
GNATprove supports the suppression of warnings and justification of check messages with pragmas inserted in the source code. But these justifications may become obsolete across time. To help with that, GNATprove now issues a warning on useless justifications.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 Johannes Kanig
SPARK 15: Errors, Warnings and Checks
The messages issued by the SPARK toolset will change a bit in the next version of both SPARK Pro and SPARK GPL. This post explains the change and the motivation behind it.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 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 Yannick Moy
Use of SPARK in a Certification Context
Using SPARK or any other formal method in a certification requires that the applicant agrees with the certification authority on the verification objectives that this use of formal methods allows to reach, and how this is obtained and documented. In order to facilitate this process, the participants to the workshop on Theorem Proving in Certification have produced a draft set of guidelines, now publicly available.by Yannick Moy
Contextual Analysis of Subprograms Without Contracts
We have implemented a new feature in GNATprove for analyzing local subprograms in the context of their calls. This makes it possible to benefit from the most precise analysis for local subprograms, without incurring the cost of adding contracts to these subprograms.by Yannick Moy
