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.
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.
Two important features that have been included respectively in SPARK Pro 15.0 (precise support for bitwise and modular arithmetic) and SPARK Pro 16.0 (generation of counterexamples) will be presented at the upcoming conferences NASA Formal Methods in June and Software Engineering and Formal Methods in July.
A recent scientific article "Progress-Sensitive Security for SPARK" by researchers Willard Rafnsson, Deepak Garg and Andrei Sabelfeld examines what it means for SPARK flow analysis to catch side-channel information leaks related to program termination.
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.
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.
This is a curious story of how a bug found by a GNAT user in the runtime library of the compiler lead us to formally verify the well-known function Ada.Text_IO.Get_Line, which reads a line of text from an input file, and to find 3 more bugs in the process.
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.
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.
The new version 16 of SPARK Pro toolset is now available for AdaCore's customers. See demo online.