Blog
An Insight Into the AdaCore Ecosystem
Announcing Advent of Ada/SPARK 2025: Coding for a Cause!
Florian Schanda
Information Flo(w): Array Initialization in Loops
SPARK only supported array initialization using aggregates, as array initialization in loops raised a false alarm in flow analysis. Read on to learn…
Florian Schanda
SPARK 2014 Rationale: Data Dependencies
Programs often use a few global variables. Global variables make passing common information between different parts of a program easier. By reading…
Gem #157: Gprbuild and Code Generation
This series of Gems explains how gprbuild can be configured to invoke code generators before it compiles the resulting code itself.
Yannick Moy
GNATprove Tips and Tricks: How to Write Loop Invariants
Having already presented in previous posts why loop invariants are necessary for formal verification of programs with loops, and what loop invariants…
Gem #156: Listing Control in GNAT
Yannick Moy
Case Study for System to Software Integrity Includes SPARK 2014
My colleague Matteo Bordin will present at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February a case study…
Claire Dross
SPARK 2014 Rationale: Verifying Properties over Formal Containers
We saw in a previous post how we could express complex properties over formal containers using quantified expressions. In this post, I present how…
Yannick Moy
Muen Separation Kernel Written in SPARK
The University of Applied Sciences Rapperswil in Switzerland has released last week an open-source separation kernel written in SPARK, which has been…
Claire Dross
SPARK 2014 Rationale: Expressing Properties over Formal Containers
We saw in a previous post how formal containers can be used in SPARK code. In this post, I describe how to express properties over the content of…
Gem #155: Enhancing the GPRBuild Database for a New Language
Yannick Moy
Rail, Space, Security: Three Case Studies for SPARK 2014
We will present three case studies using SPARK 2014 at the upcoming Embedded Real Time Software and Systems conference in Toulouse in February 2014,…
Claire Dross
SPARK 2014 Rationale: Formal Containers
SPARK 2014 excludes data structures based on pointers. Instead, one can use the library of formal containers. They are variant of the Ada 2012…