Blog
An Insight Into the AdaCore Ecosystem
Proving Safety at Scale: SPARK, RISC-V, and NVIDIA’s Security Strategy
Read More
Yannick Moy
Research Corner - SPARK 2014 vs Frama-C vs Why3
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…
Emma Adby
Introducing the Make With Ada competition!
Yannick Moy
Research Corner - Proving Security of Binary Programs with SPARK
Researchers from Dependable Computing and Zephyr Software LLC have presented at the latest NASA Formal Methods conference last week their work on…
Pierre-Marie de Rodat
C library bindings: GCC plugins to the rescue
Fabien Chouteau
Make with Ada: ARM Cortex-M CNC controller
Yannick Moy
GNATprove Tips and Tricks: Using the Lemma Library
A well-know result of computing theory is that the theory of arithmetic is undecidable. This has practical consequences in automatic proof of…
Claire Dross
Quantifying over Elements of a Container
Containers holding several items of the same type such as arrays, lists, or sets are a common occurrence in computer programs. Stating a property…
Florian Schanda
SPARKSMT - An SMTLIB Processing Tool Written in SPARK - Part I
Today I will write the first article in a short series about the development of an SMTLIB processing tool in SPARK. Instead of focusing on features,…
Emma Adby
Certification and Qualification
Jérôme Lambourg
Efficient use of Simics for testing
Emma Adby
VectorCAST/Ada: Ada 2012 Language Support
Yannick Moy
Did SPARK 2014 Rethink Formal Methods?
David Parnas is a well-known researcher in formal methods, who famously contributed to the analysis of the shut-down software for the Darlington…