Blog

Claire Dross

Contracts of Functions in SPARK 2014

In SPARK 2014, we can write a function F and annotate it with a pre and a postcondition. In this post, we explain how the SPARK 2014 proof tool…

Florian Schanda

SPARK 2014 Rationale: Information Flow

In a previous blog post we described how aspect Global can be used to designate the specific global variables that a subprogram has to read and…

Yannick Moy

Contextual Analysis of Subprograms Without Contracts

We have implemented a new feature in GNATprove for analyzing local subprograms in the context of their calls. This makes it possible to benefit from…

Johannes Kanig

Prove in Parallel with SPARK 2014

The article explains how we improved the performance of the SPARK 2014 toolset when multiple CPU cores are available for proof.

Yannick Moy

Studies of Contracts in Practice

Two recent research papers focus on how program contracts are used in practice in open source projects, in three languages that support contracts…

Johannes Kanig

A Little Exercise With Strings

I recently looked at string manipulation functions in a library and tried to prove absence of run-time errors of one of them. Although the function…

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…