AdaCore Blog

The Eight Reasons For Using SPARK

by Yannick Moy

Based on our many years of experience with our customers using SPARK in their projects, we have come up with a list of eight objectives that are most commonly targeted when using SPARK. Most projects only target a few of them, but in theory one could try to achieve all of them with SPARK on a project. This list may be useful for those who want to assess if the SPARK technology can be of benefit in their context, and to existing SPARK users to compare their existing practice with what others do. Each objective is described with some details in a separate section of the SPARK User's Guide.

Objectives 1 to 4 are applicable to most projects:

Objectives 5 to 8 address specific issues:

If you feel that your own objectives for using SPARK are not represented in the list above, please let us know. Our aim is to enrich this list in the future to represent most (if not all) SPARK projects.

Posted in #Formal Verification    #Design Method    #Certification    #SPARK   

About Yannick Moy

Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK, a product he presents in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.