spark2014

The annual release of GNAT GPL and SPARK GPL have just been announced, and can be downloaded from libre.adacore.com. For SPARK, the changes are quite noticeable, with much improved provability, automation and usability. I know some people have been waiting for it for many months, so here it is!

The annual release of GNAT GPL and SPARK GPL have just been announced, and can be downloaded from libre.adacore.com. For SPARK, the changes are quite noticeable, with much improved provability, automation and usability. I know some people have been waiting for it for many months, so here it is!

Floating point problems are difficult and interesting. This blog post describes the process of creating floating point benchmarks: one of the activities are doing to help out the SMTLIB effort (SMTLIB is the language our VCs are expressed in).

Floating point problems are difficult and interesting. This blog post describes the process of creating floating point benchmarks: one of the activities are doing to help out the SMTLIB effort (SMTLIB is the language our VCs are expressed in).

In 2010, Rod Chapman released an implementation in SPARK of the Skein cryptographic hash algorithm, and he proved that this implementation was free of run-time errors. That was a substantial effort with the previous version of the SPARK ... [More] technology. We have recently translated the code of SPARKSkein from SPARK 2005 to SPARK 2014, and used GNATprove to prove absence of run-time errors in the translated program. The difference between the two technologies is striking. The heroic effort that Rod put in the formal verification of the initial version of SPARKSkein could now be duplicated with modest effort and modest knowledge of the technology, thanks to the much greater proof automation that the SPARK 2014 technology provides, as well as various features that lower the need to provide supporting specifications, most notably contracts on internal subprograms and loop invariants. [Less]

In 2010, Rod Chapman released an implementation in SPARK of the Skein cryptographic hash algorithm, and he proved that this implementation was free of run-time errors. That was a substantial effort with the previous version of the SPARK technology. ... [More] We have recently translated the code of SPARKSkein from SPARK 2005 to SPARK 2014, and used GNATprove to prove absence of run-time errors in the translated program. The difference between the two technologies is striking. The heroic effort that Rod put in the formal verification of the initial version of SPARKSkein could now be duplicated with modest effort and modest knowledge of the technology, thanks to the much greater proof automation that the SPARK 2014 technology provides, as well as various features that lower the need to provide supporting specifications, most notably contracts on internal subprograms and loop invariants. [Less]

Our intern Anthony Leonardo Gracio has rewritten the code of the stabilization system of the Crazyflie drone, initially written in C, and verified with GNATprove that the code is free from run-time errors. Read all about it on AdaCore's blog.

Our intern Anthony Leonardo Gracio has rewritten the code of the stabilization system of the Crazyflie drone, initially written in C, and verified with GNATprove that the code is free from run-time errors. Read all about it on AdaCore's blog.