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.
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.
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.
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!
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.
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.
by
Emma Adby
–
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.
by
Emma Adby
–
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.
by
Emmanuel Briot
–
Integrate new tools in GPS (2)
Customizing build target switchesIn 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.