Fabien Chouteau

Formal verification is the act of proving the correctness of software using mathematics. That means proving that your code is free of bugs and/or follows its specifications. SPARK is both a language (subset of Ada) and a set of tools that bring automatic formal verification in the hands of any developer.

This technology is getting more interest from the industry (e.g. NVIDIA recently) for its extremely powerful properties in terms of safety and security. However, it is not widely known that SPARK is both open source and very easy to start using.

In this talk I will provide quick and easy instructions to start your first formally verified library in SPARK. Using only free and open-source tools and resources (compiler, package manager, IDE, verification tools).

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:

• Pin system: intended to help with the development and use of WIP crates.
• Crate configuration: that enables static code generation before compilation.
• Toolchains: that enable easy installation of [cross-]compiler and builder versions.
• Auto GPR with: for automatic “with”ing of dependencies.
• Etc.

We will also have a look at the ecosystem of crates available in the Alire community index.

For embedded developers using alternative programming languages, but also for anyone using third party driver frameworks such as libopencm3, one of the main pain points to start using a microcontroller is to make a Board Support Package.

Things like linker script or startup code (crt0) not only require skills, but also information that are not always easily accessible.

In this talk we will present a tool that generates linker script, startup code, and low level hardware binding for 3000+ ARM microcontrollers using information extracted from archives provided as part of the ARM Cortex Microcontroller Software Interface Standard (CMSIS).

Alire (Ada LIbrary REpository) is a package manager project for the Ada/SPARK community. The goal of a package manager is to facilitate collaboration within the community and to lower the barrier of entry for beginners.

In this talk we will present the Alire project, what it can do for you and how you can contribute and give more visibility to your Ada/SPARK projects.

We will also provide a tutorial to show how to use Alire to create a library and then publish it for others to use.

In this talk I want to open a window into the wonderful world of "alternative" programming languages for RISC-V. What can you get by looking beyond C/C++.

So I will start with a quick introduction to the Ada and SPARK languages, the benefits, the hurdles. I will also present an overview of the applications and domains where they shine, when failure is not an option.

I will then do a short getting started session and provide all the details for you to start RISC-V programming with Ada/SPARK on different platforms (QEMU, HiFive1, FPGAs with PicoRV32).

At the end of the talk, I will give my view of the RISC-V architecture and community from the perspective of an alternative languages developer. I will cover the good points, the risks, and provide some ideas on how the RISC-V can keep the door open.

O’PAVES (Open Platform for Autonomous VEhicle Systems) aims at providing an open source and open hardware platform for the prototyping and development of autonomous vehicles. In the current state of the project, what we have is a remote controlled car, but with sensors that you would find on an autonomous vehicle such as IMU and distance sensors. The goal is not necessarily to implement the autonomous feature ourselves, but to allow users to do it by either modify the firmware or add and external computer such as a Raspberry Pi or OpenMV to to add autonomous driving features.

The hardware is open and was designed with FOSS tools such as Kicad and FreeCAD. It’s made of a PCB that act as the frame of the car, 3D printed parts, off the shelf parts from pololu.com (battery, motors, sensors) and and Crazyflie 2.0 nano drone. The drone (without its motors) is connected to the O’PAVES board using an extension port. This solution makes the platform easy to build because most of the very small electronic assembly is already done on the drone. The software is developed in Ada and also only uses FOSS tools like the GNAT compiler or the AdaDriversLibrary. The project is hosted on GitHub: https://github.com/adacore/opaves

In this 25 minutes talk I want to present the state of the project, explain how you can build and hack the platform and show some of the tools and techniques that we used to develop the project. I will bring one of the prototype with me and at least show a video demo if not a live demo.

The Ada programming language was designed for embedded programming and it is well known in the aerospace domains and in general every domain where failure is not an option. Unfortunately it is not used a lot in the embedded FOSS community.

In the past two years, AdaCore worked to promote the use of Ada in the FOSS community, in particular for embedded programming with the "Make with Ada" blog post series, my "Programming is Too Difficult for Humans" interview for the Embedded.fm podcase, "Ada Driver Library" blog posts on "ARM Community", or the "Make with Ada" embedded software project competition.

In this 45 minutes lecture I will:

give a short introduction of Ada for embedded and how its features (programing by contract, strong typing, representation clauses (hardware mapping), OOP, static compiler checks and optional run-time checks) can help improving the development time, maintenance and quality of FOSS embedded projects;

present the AdaDriversLibrary project, where we put all those features in practice to develop micro-controller device drivers in Ada;

make a quick getting started demo;

present some of the best projects from the "Make with Ada" competition.

In this talk I will present the first 4 projects of the "Make with Ada" blog post series: a solenoid engine, an Apollo lunar lander simulator, a software synthesizer framework, and a formally proven smartwatch app. I will also explain the motivation behind this series, where we want to go, and the feedback we've got from it.