Florian Schanda

Florian has a background in theoretical computer science and holds a degree from the University of Bath. While his research PhD is in computer graphics, he has a wide variety of academic interests including answer set programming (ASP), graph theory, (programming) language design and compilers, cryptography and related security topics. He has joined the SPARK team of Altran in 2010.

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.