SPARK and external verification

I will give an introduction to SPARK and describe some recent work on applying external verification tools to SPARK problems. SPARK is a programming language, a set of verification tools, and a design approach for critical systems. A number of military and commercial high integrity projects, ranging from 10 000 to 5 million lines of code, are developed in SPARK. Examples include Rolls Royce Trent (engine control), EuroFighter Typhoon (military aircraft), and NATS iFACTS (air traffic control). In the iFACTS project for example, over 100 000 SPARK verification conditions (VCs) for type safety of the 180 000 lines of code are generated and discharged every night.

Praxis has several ongoing projects both to extend the SPARK language and to improve proof automation. For example I will describe how to use Victor (by Paul Jackson et al), a translator from SPARK VCs to SMT-lib queries, and the latest results of using Victor on some of Praxis' benchmarks (modern SMT solver, or a 25 year old Praxis in-house deduction prover written in prolog, who do you think wins?).