Blog
An Insight Into the AdaCore Ecosystem
Formal Methods Practice and Theory
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…
Emma Adby
Provably safe programming at Embedded World
Emma Adby
CubeSat continues to orbit the Earth thanks to Ada & SPARK!
Yannick Moy
Formal Verification of Legacy Code
Yannick Moy
SPARK Prez at New Conference on Railway Systems
RSSR is a new conference focused on the development and verification of railway systems. We will present there how SPARK can be used to write…