Ada

Proving the Correctness of GNAT Light Runtime Library

D.ada
Yannick Moy
<p>As a programming language, Ada offers a number of features that require runtime support, e.g. exception propagation or concurrency (tasks, protected objects). The GNAT compiler implements this support in its runtime library, which comes in a number of different flavors, with more or less capability. The GNAT light runtime library is a version of the runtime library targeted at embedded platforms and certification, with an Operating System or without it (baremetal). It contains around 180 units focused mostly on I/O, numerics, text manipulation, memory operations.</p> <p>Variants of the GNAT light runtime library have been certified for use at the highest levels of criticality in several industrial domains: avionics (DO-178), space (ECSS-E-ST40C), railway (EN 50128), automotive (ISO-26262). Details vary across certification regimes, but the common approach to certification used today is based on written requirements traced to corresponding tests, supported by test coverage analysis. Despite this strict certification process, some bugs were found in the past in the code. An ongoing project at AdaCore is applying formal proof with SPARK to the light runtime units, in order to prove their correctness: that the code is free of runtime errors, and that it satisfies its functional specifications.</p> <p>So far, 30 units (out of 180) have been proved, and a few bugs fixed along the way (including a security vulnerability). In this talk, I will describe the approach followed, what was achieved, and what we expect to achieve.</p>

Additional information

Type devroom

More sessions

2/6/22
Ada
Fernando Oleo Blanco
D.ada
<p>Welcome to the Ada Developer Room at FOSDEM 2020, which is organized in cooperation with Ada-Europe and Ada-Belgium.</p> <p>This year marks the first edition on which the devroom takes place on an online format. For that reason, this presentation will explain how does it work and how can the public use the systems provided by FOSDEM and interact with the speakers. We will also introduce the Ada-Europe and Ada-Belgium organisations. This small introduction also serves as a test to make sure ...
2/6/22
Ada
Jean-Pierre Rosen
D.ada
<p>An overview of the main features of the Ada language, with special emphasis on those features that make it especially attractive for free software development.</p> <p>Ada is a feature-rich language, but what really makes Ada stand-out is that the features are nicely integrated towards serving the goals of software engineering. If you prefer to spend your time on designing elegant solutions rather than on low-level debugging, if you think that software should not fail, if you like to build ...
2/6/22
Ada
Stefan Hild
D.ada
<p>In 2020 I started live streaming the development of a turn-based strategy game. At that time I had little idea about Ada, programming or game development (nothing has changed about that to this day). But by September 2020 it had taken the early form of a Civilization clone. After more than a year of development, it has become almost a real game with its own features. And now I'm going to talk a little bit about some experiences and weirdnesses with game development in Ada</p>
2/6/22
Ada
Jean-Pierre Rosen
D.ada
<p>The requirements for Ada numerics were to provide portable arithmetics without unacceptable performance cost. This talk shows how this was achieved by interval arithmetics without requiring a particular implementation model, like IEEE arithmetics.</p>
2/6/22
Ada
D.ada
<p>At FOSDEM 2020 we presented the first version of Alire, the package manager for the Ada Open Source ecosystem. Two years later, the tools and its ecosystem have evolved, in some instances based on the feedback received at FOSDEM. So we want to give you an update on the new features and improvements, including:</p> <ul> <li>Pin system: intended to help with the development and use of WIP crates.</li> <li>Crate configuration: that enables static code generation before compilation.</li> ...
2/6/22
Ada
Gabriele Galeotti
D.ada
<p>SweetAda is a lightweight development framework whose purpose is the implementation of Ada-based software systems.</p>
2/6/22
Ada
Alejandro R. Mosteo
D.ada
<p>Ada 2022 is around the corner with many goodies in the form of new features and featurettes. Arguably small syntax sugar additions combine for the programmer's comfort, like for example user-defined literals and container aggregates, that allow natural initialization of user-defined containers with the same expressions used for basic arrays since the beginnings of Ada. In this talk, I discuss how these features allow the initialization of a container data type for heterogeneous values (a-la ...