Ian Oneill
Ian is the principle author of SPARK’s proof tools, the Simplifier and Proof Checker. His work on tool-supported proof began in the 1980s, as part of Dr Bernard Carré’s software analysis and verification team at the University of Southampton. This work led to the Proof Checker, and in 1987 to its first industrial use proving properties of assembly code modules for use in a jet engine controller.
With the development of SPARK and the Examiner, and its increasing use in significant high-integrity applications, increased proof automation became vital. In the early 1990s Ian developed the Simplifier, combining elements from the Proof Checker with some additional proof strategies. Ian has been involved over the years in a number of enhancements to the SPARK proof tools, including additional numeric range-checking strategies, increased automation, and support for user-defined proof rules. He has also had significant involvement in training and support of the use of SPARK and the proof tools, which led to the Advanced SPARK Program Design and Verification course in recent years.
As well as SPARK tool-development, training and support, Ian has over two decades of involvement in high-integrity software development and real-world experience in the use of SPARK.
What does “Frontline Support” mean to you?
It’s a chance to do some problem-solving: look at an issue someone has raised, and see if I can help in some way. Sometimes, it’s explaining an aspect of the language or the tools, or suggesting an alternative means of doing something; occasionally, it leads to a potential tool enhancement which can make the user’s life easier. It’s very satisfying to feel you’ve helped someone get the most from using the tools, and if that leads to enhancements to make everyone’s life easier in the future, that’s even better.
What drew you to SPARK/Ada?
Historical accident, really! Having developed the Proof Checker, I was a software verifier in need of some interesting software to verify. When Trevor and Bernard developed SPARK, we had an industrial-strength toolset, and it was great to be able to contribute to that. It still is, in fact.
What’s your favorite feature of SPARK Pro Technology
The Proof Checker, though I appreciate it’s not everyone’s cup of tea. The Simplifier runs it a close second, but then I may be biased!
