What does “Frontline Support” mean to you?
Working with and helping users of SPARK to both resolve their problems and consequently to improve the SPARK tool-set so that they cannot happen again.
What drew you to SPARK/Ada?
SPARK is a unique system in the world of static analysis tools in that it allows partial correctness proofs for non-trivial real-world programs. This makes it a very interesting underlying system to use in research for automated program verification.
What’s your favorite feature of SPARK Pro Technology
Philosophically, that the entire tool chain is available under the GPL license.
Technically, the fact that SPARK uses an intermediate language (FDL) to represent a language-neutral model of the program. All proofs are based on models expressed in this language, which opens up the door for further research and alternative and complementary program verification technology.