User:PhilThornley: Difference between revisions
Content added Content deleted
(Created page with '{{mylangbegin}} {{mylang|Ada|Competent}} {{mylang|SPARK|Expert}} {{mylangend}} =My Experience= Almost all my experience is in the field of embedded systems. <p>Since 1992 I have …') |
|||
| Line 5: | Line 5: | ||
=My Experience= |
=My Experience= |
||
Almost all my experience is in the field of embedded systems. |
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 [http://www.sparksure.com/ SparkSure] home page. |
|||
==SPARK Proof== |
==SPARK Proof== |
||
I have a particular interest in the use of SPARK for the formal proof of program properties and I have written [http://www.sparksure.com/5.html some tutorials] on this. |
I have a particular interest in the use of SPARK for the formal proof of program properties and I have written [http://www.sparksure.com/5.html 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. |
|||
Latest revision as of 09:02, 18 August 2010
| 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.