spark2014

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.

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.

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 ... [More] 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. [Less]

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 ... [More] 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. [Less]

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 ... [More] 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. [Less]

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 ... [More] 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. [Less]

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.

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.