AdaCore Blog

An Insight Into the AdaCore Ecosystem

by Fabien Chouteau, Yannick Moy, Vasiliy Fofanov, Nicolas Setton

A Modern Syntax for Ada

One of the most criticized aspect of the Ada language throughout the years has been its outdated syntax. Fortunately, AdaCore decided to tackle this issue by implementing a new, modern, syntax for Ada.

#Ada    #GPS    #Language   

by Jamie Ayre

Welcoming New Members to the GNAT Pro Family

As we see the importance of software grow in applications, the quality of that software has become more and more important. Even outside the mission- and safety-critical arena customers are no longer accepting software failures (the famous blue screens of death, and there are many...). Ada has a very strong answer here and we are seeing more and more interest in using the language from a range of industries. It is for this reason that we have completed our product line by including an entry-level offer for C/C++ developers wanting to switch to Ada and reinforced our existing offer with GNAT Pro Assurance for programmers building the most robust software platforms with life cycles spanning decades.

#GNAT Pro    #Ada   

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.

#GNAT     #typing   

by Pierre-Marie de Rodat, Nicolas Setton

GNAT GPL 2017 is out!

For those users of the GNAT GPL edition, we are pleased to announce the availability of the 2017 release of GNAT GPL and SPARK GPL.

#GNAT GPL   

by Yannick Moy

Research Corner - Floating-Point Computations in SPARK

It is notoriously hard to prove properties of floating-point computations, including the simpler bounding properties that state safe bounds on the values taken by entities in the program. Thanks to the recent changes in SPARK 17, users can now benefit from much better provability for these programs, by combining the capabilities of different provers. For the harder cases, this requires using ghost code to state intermediate assertions proved by one of the provers, to be used by others. This work is described in an article which was accepted at VSTTE 2017 conference.

#Formal Verification    #SPARK   

by Yannick Moy

New Guidance for Adoption of SPARK

While SPARK has been used for years in companies like Altran UK, companies without the same know-how may find it intimidating to get started on formal program verification. To help with that process, AdaCore has collaborated with Thales throughout the year 2016 to produce a 70-pages detailed guidance document for the adoption of SPARK. These guidelines are based on five levels of assurance that can be achieved on software, in increasing order of costs and benefits: Stone level (valid SPARK), Bronze level (initialization and correct data flow), Silver level (absence of run-time errors), Gold level (proof of key properties) and Platinum level (full functional correctness). These levels, and their mapping to the Development Assurance Levels (DAL) and Safety Integrity Levels (SIL) used in certification standards, were presented at the recent High Confidence Software and Systems conference.

#Formal Verification    #SPARK   

by Anthony Leonardo Gracio

GPS for bare-metal developers

In my previous blog article, I exposed some techniques that helped me rewrite the Crazyflie’s firmware from C into Ada and SPARK 2014, in order to improve its safety.

#GPS    #Embedded Development    #Makers   

by Pierre-Marie de Rodat

GNATcoverage moves to GitHub

Following the current trend, the GNATcoverage project moves to GitHub! Our new address is: https://github.com/AdaCore/gnatcoverage

#GitHub    #GNATcoverage   

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

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

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.

#AdaCoreTechDay    #GNAT     #Embedded Development    #embedded   

by AdaCore Admin

QGen 2.1 Release!

Embedded World will see the latest release of QGen, the qualifiable and customisable code generator for Simulink® and Stateflow® models!

#QGen    #QGen2.1    #AdaCoreTechDay    #Embedded World    #emb2016   

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.

#SPARK Pro    #SPARK2014     #SPARKPro16   

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.

#Language    #Formal Verification    #SPARK   

by Florian Schanda

SPARK 2016 Supports Ravenscar!

The new big feature of the SPARK 2016 release is the support of the Ravenscar profile. Users can now use protected objects and tasks to write concurrent code. On uniprocessor computers the toolset can ensure that no deadlocks or data races will occur and that no tasks will terminate. Read this blog post to learn more and see the new feature in practice.

#Language    #Formal Verification    #SPARK   

by David Hauzar

SPARK 16: Generating Counterexamples for Failed Proofs

While the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would automatically find values of variables showing why a proof fails. SPARK Pro 16, to be released in 2016, is going to introduce such a feature. If a proof fails, it attempts to generate a counterexample exhibiting the problem. This post introduces this new feature, developed in the scope of the ProofInUse laboratory.

#Formal Verification    #SPARK   

by Yannick Moy

GNATprove Tips and Tricks: User Profiles

One of the most difficult tasks when using proof techniques is to interact with provers, in particular to progressively increase proof power until everything that should be proved is proved. Until the last release, increasing the proof power meant operating on three separate switches. There is now a simpler solution based on a new switch --level, together with a simpler proof panel in GPS for new users.

#Formal Verification    #SPARK   

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.

#OSS    #IoT    #Programming     #HIS   

by AdaCore Admin

AdaCore Tech Days 2015

#AdaCoreTechDay    #GNAT Pro    #CodePeer    #SPARK Pro    #SPARK    #QGen   

by Florian Schanda

SPARK 2014 Rationale: Variables That Are Constant

The SPARK tools now support yet another feature that allows users to better specify the intended behavior of their programs. This new feature enables users to declare that specific variables can only be updated during the elaboration of their enclosing package. Read on if you want to know more...

#Formal Verification    #Language    #SPARK   

by Yannick Moy

New Book About SPARK 2014

I am very pleased to announce that a book is now available for those who want to learn formal verification with SPARK 2014. This book was written by Prof. John McCormick from University of Northern Iowa and Prof. Peter Chapin from Vermont Technical College. We've been interacting a lot with them since they started in 2013, and the result of these interactions is quite satisfying!

#SPARK    #Formal Methods    #Teaching   

by Olivier Ramonat

AdaCore Releases GNAT Pro 7.3, QGen 1.0 and GNATdashboard 1.0

February saw the annual customer release of a number of important products. This is no mean task when you consider the fact that GNAT Pro is available on over 50 platforms and supports over 150 runtime profiles (ranging from Full Ada Support to the very restricted Zero Footprint Profile suitable for safety-critical development). All in all, from the branching of the preview version to the customer release it takes us nearly 4 months to package everything up! Quality is assured through the internally developed AdaCore Factory.

#GNAT Pro    #SPARK Pro    #GPS    #GNATbench    #GNATdashboard    #Ada    #AdaCore Factory    #CodePeer    #QGen   

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.

#Formal Verification    #SPARK   

by AdaCore Admin

A Busy Schedule Ahead!

If you have a passion for Ada, need more information on our technology or would just like to have a chat, there are a couple of upcoming events where we'd love to meet up. What's more, we'll be launching our brand new product QGen at Embedded World!

#Ada    #Embedded World    #Certification Together    #QGen   

by Yannick Moy

Using Coq to Verify SPARK 2014 Code

In the first release of SPARK 2014, GNATprove only provided support for automatic provers, in particular Alt-Ergo. Automatic provers are very handy when it comes to perform a big numberof simple proof. But they can fail to prove valid formulas when the proof involves some advanced reasoning. As mentioned in a previous post, one check left unproved might invalidate assumptions on which are based the proofs of multiple other checks. This is a case where manual proof may be useful for SPARK 2014 users. The development version of GNATprove now supports Coq to perform manual proof.

#Formal Verification    #SPARK   

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.

#Formal Verification    #SPARK   

by Yannick Moy

Short Video Demo of SPARK 2014

New to SPARK? Want to "see" what's new in SPARK 2014? It's all in this 5 mn video demo!

#Formal Verification    #Language    #SPARK   

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.

#Formal Verification    #SPARK   

by Yannick Moy

SPARK 2014 Rationale: Mixing SPARK and Ada Code

The first step before any formal verification work with SPARK is to delimitate the part of the code that will be subject to formal verification within the overall Ada application. This post presents the solution we've come up with for SPARK 2014.

#Language    #Formal Verification    #SPARK   

by Florian Schanda

SPARK 2014 Flow Analysis

We have nearly finished implementing a central component of the SPARK 2014 analysis tools: the flow analysis engine; so this is a good time to introduce some of the analysis it will carry out.

#Language    #SPARK   

by Yannick Moy

Project Hi-Lite Wrap-up

After three years of hard work, we have reached last week the end of project Hi-Lite, whose goal was to simplify the use of formal methods. We're proud to publicize the results obtained, in particular the new version of SPARK and the associated tool GNATprove. Here's a summary of the wrap-up meeting.

#Formal Verification    #SPARK