Blog

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…

Yannick Moy

GNATprove Tips and Tricks: Referring to Input in Contracts

In a previous post about pre-call values, I described how the Ada language rules implemented in the compiler prevent surprises when referring to…

Yannick Moy

SPARK 2014 Rationale: Global State

Global variables are a common source of programming errors: they may fail to be initialized properly, they can be modified in unexpected ways,…