User:PhilThornley
Appearance
My Favorite Languages | |
Language | Proficiency |
Ada | Competent |
SPARK | Expert |
My Experience
Almost all my experience is in the field of embedded systems.
Since 1992 I have worked on high-integrity applications, with most of that work using SPARK. Further information can be found at my SparkSure home page.
SPARK Proof
I have a particular interest in the use of SPARK for the formal proof of program properties and I have written some tutorials on this.
SPARK is a uniquely capable language for proof as it can be used for industrial scale applications but is also a completely unambiguous language - so formal proofs become meaningful.