Blog
An Insight Into the AdaCore Ecosystem
Formal Methods Practice and Theory
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,…
Gem #154: Multicore Maze Solving, Part 2
Yannick Moy
SPARK 2014 Rationale: Mixing SPARK and Ada Code
The first step before any formal verification work with SPARK is to delimitate the part of the code that will be subject to formal verification…
Gem #153: Multicore Maze Solving, Part 1
Yannick Moy
SPARK 2014 Rationale: Loop Variants
Loop variants are the little-known cousins of the loop invariants, used for proving termination of subprograms. Although they may not look very…