Blog
An Insight Into the AdaCore Ecosystem
Proving Safety at Scale: SPARK, RISC-V, and NVIDIA’s Security Strategy
Read More
Yannick Moy
GNATprove Tips and Tricks: What’s Provable for Real?
SPARK supports two ways of encoding reals in a program: the usual floating-point reals, following the standard IEEE 754, and the lesser known…
Yannick Moy
SPARK 2014 Rationale: Support for Ravenscar
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…
Emmanuel Briot
Calling inherited subprograms in Ada
This short post describes an idiom that can be used to help maintain complex hierarchies of tagged types, when methods need to call the parent types…
Florian Schanda
SPARK 2016 Supports Ravenscar!
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…
Fabien Chouteau
Make with Ada: Formal proof on my wrist
When the Pebble Time kickstarter went through the roof, I looked at the specification and noticed the watch was running on an STM32F4, an ARM…
Emma Adby
Modernizing Adacore's Open-Source Involvement
David Hauzar
SPARK 16: Generating Counterexamples for Failed Proofs
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…
Emma Adby
ARM TechCon and NBAA Conference 2015
Yannick Moy
GNATprove Tips and Tricks: User Profiles
One of the most difficult tasks when using proof techniques is to interact with provers, in particular to progressively increase proof power until…
Maxim Reznik, Nicolas Setton
Using reference types to handle persistent objects
Emma Adby
HIS Conference 2015, Bristol
Emma Adby