SPARK 2014

Expanding the boundaries of safe and secure programming.

Learn more about SPARK 2014

Videos

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.

Integrating Proof and Testing in Verification Strategies for Safety Critical Systems

by Admin in Videos – February 23, 2013

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 sense and can bring significant cost savings, without forcing dramatic changes in internal development procedures.

SPARK 2014 – Future directions

by Admin in Videos – February 23, 2013

Stuart Mathews gave this talk at the recent SPARK User Group. In it he presents the next generation of the SPARK language which will extend the range of programs that can be automatically verified and provides an innovative means for combing formal verification and testing.

Directions in Secure Software Development

by Admin in Videos – February 22, 2013

Rod Chapman, Altran Praxis, gave this talk at the recent SPARK User Group. This talk reflected on our experiences with building secure systems with SPARK and other formal methods, including the lessons learned from the MULTOS CA, Tokeneer and SPARKSkein projects, and the relationship between safety- and security-critical development.