spark2014

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

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

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

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

The new big feature of the SPARK 2016 release is the support of the Ravenscar profile. Users can now use protected objects and tasks to write concurrent code. On uniprocessor computers the toolset can ensure that no deadlocks or data races ... [More] will occur and that no tasks will terminate. Read this blog post to learn more and see the new feature in practice. [Less]

The new big feature of the SPARK 2016 release is the support of the Ravenscar profile. Users can now use protected objects and tasks to write concurrent code. On uniprocessor computers the toolset can ensure that no deadlocks or data races will occur ... [More] and that no tasks will terminate. Read this blog post to learn more and see the new feature in practice. [Less]

While the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would automatically find values of variables showing why a proof fails. SPARK Pro 16, to be released in 2016 ... [More] , is going to introduce such a feature. If a proof fails, it attempts to generate a counterexample exhibiting the problem. This post introduces this new feature, developed in the scope of the ProofInUse laboratory. [Less]

While the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would automatically find values of variables showing why a proof fails. SPARK Pro 16, to be released in 2016, is ... [More] going to introduce such a feature. If a proof fails, it attempts to generate a counterexample exhibiting the problem. This post introduces this new feature, developed in the scope of the ProofInUse laboratory. [Less]

One of the most difficult tasks when using proof techniques is to interact with provers, in particular to progressively increase proof power until everything that should be proved is proved. Until the last release, increasing the proof power meant ... [More] operating on three separate switches. There is now a simpler solution based on a new switch --level, together with a simpler proof panel in GPS for new users. [Less]

One of the most difficult tasks when using proof techniques is to interact with provers, in particular to progressively increase proof power until everything that should be proved is proved. Until the last release, increasing the proof power ... [More] meant operating on three separate switches. There is now a simpler solution based on a new switch --level, together with a simpler proof panel in GPS for new users. [Less]