Blog
An Insight Into the AdaCore Ecosystem
Formal Methods Practice and Theory
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
AdaCore Tech Days 2015
Florian Schanda
SPARK 2014 Rationale: Variables That Are Constant
The SPARK tools now support yet another feature that allows users to better specify the intended behavior of their programs. This new feature enables…
Yannick Moy
The Eight Reasons For Using SPARK
Based on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most…
Emmanuel Briot
Traits-Based Containers
This post describes the design of a new containers library. It highlights some of the limitations of the standard Ada containers, and proposes a new…
Yannick Moy
New Book About SPARK 2014
I am very pleased to announce that a book is now available for those who want to learn formal verification with SPARK 2014. This book was written by…