AdaCore Blog

An Insight Into the AdaCore Ecosystem

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 Claire Dross –

Research Corner - Auto-active Verification in SPARK

GNATprove performs auto-active verification, that is, verification is done automatically, but usually requires annotations by the user to succeed. In SPARK, annotations are most often given in the form of contracts (pre and postconditions). But some language features, in particular ghost code, allow proof guidance to be much more involved. In a paper we are presenting at NASA Formal Methods symposium 2017, we describe how an imperative red black tree implementation in SPARK was verified using intensive auto-active verification.

#Formal Verification    #SPARK   

by Yannick Moy –

Rod Chapman on Software Security

Rod Chapman gave an impactful presentation at Bristech conference last year. His subject: programming Satan's computer! His way of pointing out how difficult it is to produce secure software. Of course, it would not be Rod Chapman if he did not have also a few hints at how they have done it at Altran UK over the years. And SPARK is central to this solution, although it does not get mentioned explicitly in the talk! (although Rod lifts the cover in answering a question at the end)

#Security    #SPARK   

by AdaCore Admin –

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.

#SPARK    #Events   

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.

#Ada    #Devices    #drivers    #STM32    #embedded   

by Yannick Moy –

Proving Tetris With SPARK in 15 Minutes

I gave last week a 15-minutes presentation at FOSDEM conference of how you can prove interesting properties of Tetris with SPARK. Here is the recording.

#SPARK    #FOSDEM   

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

#Static Analysis   

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.

#Formal Verification    #SPARK   

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.

#Ada    #tooling   

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.

#VerificationTools    #Formal Methods    #SPARK   

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!

#Formal Verification    #SPARK   

by Yannick Moy –

SPARK Cheat Sheets (en & jp)

The SPARK cheat sheet usually distributed in trainings has recently been translated to Japanese. Here they are, both in English and in Japanese. My modest Xmas present.

#SPARK   

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.

#Makers    #Ada    #STM32    #ARM    #Embedded Development   

by AdaCore Admin –

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.

#Formal Methods    #SPARK   

by AdaCore Admin –

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.

#Formal Verification    #SPARK   

by Emmanuel Briot –

Integrate new tools in GPS (2)

Customizing build target switches In the first post in this series (Integrate new tools in GPS) we saw how to create new build targets in GPS to spawn external tools via a menu or toolbar button, and then display the output of that tool in its own console, as well as show error messages in the Locations view.

#GPS   

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.

#Formal Verification    #SPARK   

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.

#Formal Verification    #SPARK   

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.

#GPS   

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.

#Bareboard    #Embedded Development    #STM32    #Ada   

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.

#SPARK   

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.

#Language    #Formal Verification    #SPARK   

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.

#AdaCore Factory   

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.

#SPARK   

by Emmanuel Briot –

GNAT On macOS Sierra

GNAT and all the tools work great on the newly released macOS Sierra, but gdb needs some tweaking of the system.

#osx    #gdb   

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.

#SPARK    #Formal Methods   

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.

#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?

#Formal Verification    #SPARK   

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.

#GitHub    #Ada    #GNAT    

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.

#GPS    #GitHub   

by Emmanuel Briot –

Bookmarks in the GNAT Programming Studio (GPS)

As we improve existing views in GPS, we discover new ways to use them. This post shows some of the improvements done recently in the Bookmarks view, and how you can now use it as a TODO list.

#GPS   

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.

#Formal Verification    #SPARK   

by Yannick Moy –

Research Corner - SPARK 2014 vs Frama-C vs Why3

Ready for a bloody comparison between technologies underlying the tools for SPARK 2014 vs Frama-C vs Why3? Nothing like that in that article we wrote with developers of the Why3 and Frama-C toolsets. In fact, it's a bloody good comparison really, that emphasizes the differences and benefits in each technology.

#Formal Verification    #SPARK   

by AdaCore Admin –

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!

#MakewithAda    #embedded    #SPARK     #Ada   

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.

#Formal Verification    #SPARK    #Security   

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!

#Code generation    #Ada   

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.

#Makers    #Ada    #STM32    #ARM    #Embedded Development   

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.

#Formal Verification    #SPARK   

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.

#Formal Verification    #SPARK   

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.

#Dev Projects    #Formal Verification    #SPARK   

by AdaCore Admin –

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.

#TechDay    #Certification    #CodePeer   

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.

#Simics    #WindRiver    #GNAT Pro   

by AdaCore Admin –

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

#Formal Verification    #SPARK   

by AdaCore Admin –

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.

#ARM    #emb2016    #embedded    #Embedded World   

by AdaCore Admin –

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.

#Ada    #SPARK     #Space    #TechDay   

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.

#SPARK    #Legacy    #Formal Methods   

by Yannick Moy –

SPARK Prez at New Conference on Railway Systems

RSSR is a new conference focused on the development and verification of railway systems. We will present there how SPARK can be used to write abstract software specifications, whose refinement in terms of concrete implementation can be proved automatically using SPARK tools.

#SPARK   

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.

« Previous Page Next Page »