by Yannick Moy
in Formal Verification
– September 22, 2016
Something that many developers do not realize is the number of run-time checks that occur in innocent looking arithmetic expressions. Of course, everyone knows about overflow checks and range checks (although many people confuse them) and division by zero. After all, these are typical errors that do show up in programs, so programmers are aware that they should keep an eye on these. Or do they?
by Johannes Kanig
in Dev Projects, Open Source, News
– September 7, 2016
The repository on the open-do forge is now obsolete. SPARK2014 and its components Why3, Alt-Ergo, CVC4 and Z3 are available on github.
by Claire Dross
in Formal Verification
– July 26, 2016
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.
by Yannick Moy
in Formal Verification, Papers and Slides
– July 11, 2016
Ready for a bloody comparison between technologies underlying the tools for SPARK 2014 vs Frama-C vs Why3? Nothing like that in that article we wrote with developers of the Why3 and Frama-C toolsets. In fact, it's a bloody good comparison really, that emphasizes the differences and benefits in each technology.
by Yannick Moy
in Events
– June 20, 2016
AdaCore has launched the "Make with Ada" competition just today: teams of up to four have until September 30th to submit projects in Ada or SPARK which will be evaluated by a jury of four personalities of the embedded software domain: Bill Wong, Jack Ganssle, Dick Selwood and Cyrille Comar. The 5 prices range from a Crazyflie nano-copter to 5000 euros.
by Yannick Moy
in Formal Verification, Papers and Slides
– June 16, 2016
Researchers from Dependable Computing and Zephyr Software LLC have presented at the latest NASA Formal Methods conference last week their work on proving security of binary programs. In this work, they use SPARK as intermediate language and GNATprove as proof tool, which is an atypical and interesting use of the SPARK technology.
by Yannick Moy
in News
– June 1, 2016
The annual releases of GNAT GPL and SPARK GPL have just been announced, and can be downloaded from libre.adacore.com. For SPARK, this means support of concurrency with Ravenscar, generation of counterexamples and better proof automation. Enjoy!
by Yannick Moy
in Formal Verification
– May 25, 2016
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.
by Claire Dross
in Formal Verification
– May 17, 2016
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.
by Yannick Moy
in Formal Verification, Papers and Slides
– May 13, 2016
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.