SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Events

Rod Chapman on Software Security

by Yannick Moy in Events, Videos – March 7, 2017

Rod Chapman gave an impactful presentation at Bristech conference last year. His subject: programming Satan's computer! His way of pointing out how difficult it is to produce secure software. Of course, it would not be Rod Chapman if he did not have also a few hints at how they have done it at Altran UK over the years. And SPARK is central to this solution, although it does not get mentioned explicitly in the talk! (although Rod lifts the cover in answering a question at the end)

Webcast on SPARK Hosted by Electronic Design

by Yannick Moy in Events – December 6, 2016

Next Monday, Bill Wong from Electronic Design will host a free webcast on "Building High-Assurance Software without Breaking the Bank", with SPARK experts Rod Chapman and myself as presenters. You can already register for the event.

Make with SPARK

by Yannick Moy in Events – June 20, 2016

AdaCore has launched the "Make with Ada" competition just today: teams of up to four have until September 30th to submit projects in Ada or SPARK which will be evaluated by a jury of four personalities of the embedded software domain: Bill Wong, Jack Ganssle, Dick Selwood and Cyrille Comar. The 5 prices range from a Crazyflie nano-copter to 5000 euros.

AdaCore Tech Days Prez on SPARK

by Yannick Moy in Events, Videos – February 19, 2016

Hristian Kirtchev, who leads the developments of the GNAT compiler frontend, gave a very clear presentation of SPARK at the last AdaCore Tech Days in Boston. This was recorded, here is the video.

Towards SPARK Pro 16.0 And Beyond…

by Yannick Moy in Events – July 9, 2015

The international team developing the SPARK product, usually dispersed across continents and islands (if UK still counts as an Island despite the Channel Tunnel), has gathered the last week of June to discuss the progress towards SPARK Pro 16.0, and beyond that. Here are the main points that we discussed.

Pardon my French: Test et M├ęthodes Formelles

by Yannick Moy in Events – April 1, 2015

After following for two years the very interesting French conference "Forum M├ęthodes Formelles", I am now part of the program committee, so will report on interesting topics to SPARK users. The next one is on test and formal methods.

The Kickoff Meeting of the SOPRANO project

by Johannes Kanig in Formal Verification, Events – January 23, 2015

The SOPRANO project is a research project funded by the ANR (French National Research Agency) whose aim is to improve automatic proof in specific problem domains where current automatic provers are weak or have blind spots. If successful, the project will result in more proved VCs in the SPARK toolset, better counterexamples and overall easier handling of the tools. The Kickoff Meeting of SOPRANO was held on Wednesday, Jan 15th 2015, at the CEA NanoInnov building.

One Day Workshop Around SMT Solvers for ProofInUse Kickoff

by Yannick Moy in Events – December 15, 2014

To mark the start of the joint lab ProofInUse between Inria and AdaCore, whose purpose is to co-develop the SPARK and Why3 technologies, we will be hosting a one-day workshop around SMT solvers on Monday, February 2nd 2015, in the center of Paris. Registration if free but mandatory to attend the event.