I gave last week a 15-minutes presentation at FOSDEM conference of how you can prove interesting properties of Tetris with SPARK. Here is the recording.
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.
The new version 16 of SPARK Pro toolset is now available for AdaCore's customers. See demo online.
AdaCore University is hosting a 5-lessons course on SPARK 2014, which gives a complete overview of the technology.
New to SPARK? Want to "see" what's new in SPARK 2014? It's all in this 5 mn video demo!
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.
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.
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.
A presentation by Yannick Moy, Senior Engineer, AdaCore, at a recent talk at IRILL Days 2010. Video courtesy of IRILL.
Rustan Leino, a researcher at Microsoft Research, has started creating a set of videos where he both teaches and demoes how to do code verification with the tools developed at Microsoft Research.