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..

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.

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.

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.

Ten Years of Using SPARK to Build CubeSat Nano Satellites With Students

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.

Learn.adacore.com is here

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.

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!

Ada on the first RISC-V microcontroller

Updated July 2018

New strings package in GNATCOLL

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!

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.

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.

Unity & Ada

SPARKSMT - An SMTLIB Processing Tool Written in SPARK - Part I

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.

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.

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.

2015: A Space Ada‑ssey

Make with Ada: "The Eagle has landed"

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.

Larger than it looks (storage pools)

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!

Project P Open Workshop

Project-P Open Workshop

20 years on...

20 Years of AdaCore: Company as Committed as Ever on Safety-Critical Software Solutions

ProofInUse is coming!

For lovers of verification tools and critical system (we know you're out there!), we are very excited to present ProofInUse!

SPARK 2014 Rationale: Object Oriented Programming

Rail, Space, Security: Three Case Studies for SPARK 2014

SPARK 2014 goes to Space!