Author Archives: Jamie Ayre

SPARK Formal


Posted in Open-DO News | Leave a comment

Interesting new UK conference

HIS 2014 is announced as “the UK conference for sharing information about the key challenges and recent developments in high integrity software engineering. This one day conference will be held in Bristol, UK on 23rd October 2014 and will feature presentations on current industrial experience as well as keynote talks from leading industry experts.”

An interesting [...]

Posted in Certification, Events | Leave a comment

Parallel Programming Languages Enable Safer Systems

Languages that use garbage collection pose tricky issues for military system developers. In this recent article COTS journal article, Tucker Taft looks at innovative new parallel programming techniques that offer a safer solution.

Posted in Certification | Leave a comment

Software Glitches: Why We Shouldn’t Put Up With Them

Robert Dewar discusses why software glitches are unacceptable in this day and age. Software Glitches: Why We Shouldn’t Put Up With Them

Posted in In the Press | Leave a comment

Muen Separation Kernel

The Institute for Internet Technologies and Applications at the University of Applied Science in Rapperswil (Switzerland) and AdaCore today announced a significant expansion of the Open Source software model into the domain of high-assurance systems with the preview release of the Muen Separation Kernel. The Muen Kernel enforces a strict and robust isolation of components [...]

Posted in Open Source, Related Initiatives | Leave a comment

Trusted Key Manager for IKEv2

The HSR University of Applied Sciences in Switzerland has implemented the TKM from scratch using the Ada programming language. The new Design-by-Contract feature of Ada 2012 has been used for the implementation of state machines, to augment the confidence of operation according to the specification. The TKM works in conjunction with the strongSwan IKEv2 daemon [...]

Posted in Open Source | Leave a comment

Sparkel Programming Language

Sparkel is a new parallel programming language inspired by the SPARK subset of Ada, and designed to support the development of inherently safe and secure, highly parallel applications that can be mapped to multicore, manycore, heterogeneous, or distributed architectures.

To learn more about Sparkel and to follow the project, please visit

Posted in Open-DO News | Leave a comment

Ada for the C++ or Java Developer

This document will present the Ada language using terminology and examples that are familiar to developers that understand the C++ or Java languages.

To download the booklet, please visit this page

Posted in Open-DO News | 1 Comment

Safe and Secure Software – An Invitation to Ada 2012

The aim of this booklet is to show how the study of Ada in general, and the features introduced by Ada 2005 and Ada 2012 in particular, can help anyone designing safe and secure software regardless of the programming language in which the software is eventually written. After all, successful implementers of safe and secure [...]

Posted in Certification, Papers and Slides | Leave a comment

Integrating Proof and Testing in Verification Strategies for Safety Critical Systems

This talk was given by Cyrille Comar at the recent SPARK User Group. This talk reviews the prominent place and role testing holds in Safety Standards. It compares the strengths and weaknesses of testing with an alternative verification technique based on formal methods. It then explores specific instances where a combination of both approaches makes [...]

Posted in Open-DO News | 2 Comments
  • Categories

  • Open-DO Projects

  • Contact

    info @