SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

SPARKSMT - An SMTLIB processing tool written in SPARK - Part I

by Florian Schanda in Dev Projects, Formal Verification – April 21, 2016

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.

Did SPARK 2014 Rethink Formal Methods?

by Yannick Moy in Formal Verification, Papers and Slides – April 3, 2016

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.

AdaCore Tech Days Prez on SPARK

by Yannick Moy in Events, Videos – February 19, 2016

Hristian Kirtchev, who leads the developments of the GNAT compiler frontend, gave a very clear presentation of SPARK at the last AdaCore Tech Days in Boston. This was recorded, here is the video.

Christmas Elf Learns SPARK to Automate Toy Delivery by Drone

by Yannick Moy in News – December 14, 2015

To participate in the worldwide effort against global warming, Santa Claus has decided this year to retire his sleight pulled by 1024 reindeers (whose gas emitted at high altitude was threatening to put a premature end to winter season). I have been training some his Christmas elfs to build safe drones which will enter chimneys all over the world to deliver toys to kids. At least some of it is true...

GNATprove Tips and Tricks: What’s Provable for Real?

by Yannick Moy in Formal Verification – November 30, 2015

SPARK supports two ways of encoding reals in a program: the usual floating-point reals, following the standard IEEE 754, and the lesser known fixed-point reals, called this way because their precision is fixed (contrary to floating-points whose precision varies with the magnitude of the encoded number). This support is limited in some ways when it comes to proving properties of computations on real numbers, and these limitations depend strongly in the encoding chosen. In this post, I show the results of applying GNATprove on simple programs using either floating-point or fixed-point reals, to explain these differences.

SPARK 2014 Rationale: Support for Ravenscar

by Yannick Moy in Language, Formal Verification – November 23, 2015

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.