From: Tim Rowe <spamtrap@tgrowe.plus.net>
Subject: Re: ANN: SPARK Proof - Tutorials and Tools
Date: Mon, 23 Mar 2009 19:38:50 +0000
Date: 2009-03-23T19:38:50+00:00 [thread overview]
Message-ID: <_tWdna03KMnJeFrUnZ2dnUVZ8uOdnZ2d@posted.plusnet> (raw)
In-Reply-To: <b+M9J4BFcjwJJw2$@diphi.demon.co.uk>
JP Thornley wrote:
> I have put a couple of tutorials on SPARK proof onto www.sparksure.com;
> one for proof of absence of run-time error (ie using the optional proof
> annotations) and one for using the Proof Checker. Both tutorials contain
> several sections, with worked examples and exercises.
A bit of nostalgia for me there! I did the PVL SPADE course about 19
years ago, but hardly used it because my employer at the time turned out
not to have a lot of application for it. A lot of SPARK seems oddly
familiar :-)
prev parent reply other threads:[~2009-03-23 19:38 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-03-19 12:13 ANN: SPARK Proof - Tutorials and Tools JP Thornley
2009-03-20 16:31 ` John McCormick
2009-03-23 14:55 ` Michael
2009-03-23 19:38 ` Tim Rowe [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox