SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014


Prove in the Cloud

by Yannick Moy in News – October 18, 2017

We have put together a byte (8 bits) of examples of SPARK code on a server in the cloud. The benefit with this webpage is that anyone can now experiment live with SPARK without installing first the toolset. Something particularly interesting for academics is that all the code for this widget is open source. So you can setup your own proof server for hands-on sessions, with your own exercises, in a matter of minutes.

SPARK for Agile High-Integrity Development in CACM

by Yannick Moy in News, Papers and Slides – September 25, 2017

Rod Chapman, Neil White and Jim Woodcock are describing the processes that Altran has put in place over the years in its use of agile for developing high-integrity software, where automated formal verification with SPARK plays an important role. Read all about it in the latest issue of Communications of the ACM.

SPARK Discovery GPL 2017 Is Available

by Yannick Moy in Formal Verification, News – June 15, 2017

SPARK Discovery GPL 2017 is out! With more automation of proofs, new modes of user interaction, support for type invariants. Note that the optional provers CVC4 and Z3 are no longer distributed with SPARK Discovery GPL 2017, and should be installed separately.

Frama-C & SPARK Day Slides and Highlights

by Yannick Moy in News, Papers and Slides – June 2, 2017

The Frama-C & SPARK Day this week was a very successful event gathering the people interested in formal program verification for C programs (with Frama-C) and for Ada programs (with SPARK). Here is a summary of what was interesting for SPARK users. We also point to the slides of the presentations.

Make with Ada (or SPARK) is Starting Now!

by Yannick Moy in Events, News – May 12, 2017

The annual competition "Make with Ada" is starting now. Participants have until Septembre 15th to create an embedded application in Ada or SPARK, using the tools and support we'll put in place for this event. The prizes range from 5000 euros (5500 dollars) to 1000 euros (1100 dollars).

Research Corner - SPARK on Lunar IceCube Micro Satellite

by Yannick Moy in News, Papers and Slides – November 9, 2016

Researchers Carl Brandon and Peter Chapin recently presented during conference HILT 2016 their ongoing work to build a micro satellite called Lunar IceCube that will map water vapor and ice on the moon. In their paper, they explain how the use of proof with SPARK is going to help them get perfect software in the time and budget available.