From: Rod Chapman <rod@praxis-cs.co.uk>
Subject: Re: JOB:Sr. SW Engineers Wanted-Fortune 500 Co
Date: 2000/02/02
Date: 2000-02-02T00:00:00+00:00 [thread overview]
Message-ID: <3897F502.1484544E@praxis-cs.co.uk> (raw)
In-Reply-To: t7hffs6cak.fsf@calumny.jyacc.com
> When you develop pacemaker software in Ada, you still must scrutinize the
> code to insure that runtime exceptions will never happen.
There's an alternative...we now have the tools do construct
proofs that exceptions are never raised, and thus we can
_justifiably_ turn off checks. Proofs are (given some
reasaonable failure hypothesis) valid for all input data.
It also (surprisingly) turns out that the proof work was _more_
cost effective than unit testing on one project - see our paper
in FM'99 for details.
This stuff really works, and we've done it on several large
projects, mostly in the safety-critical aerospace arena. Most
people seem to think that program proofs on reasonable size
projects is impossible, perhaps owing to bad experiences
on University courses (just like me!)
- Rod Chapman
next prev parent reply other threads:[~2000-02-02 0:00 UTC|newest]
Thread overview: 44+ messages / expand[flat|nested] mbox.gz Atom feed top
2000-01-30 0:00 JOB:Sr. SW Engineers Wanted-Fortune 500 Co Tracy Goembel
2000-01-31 0:00 ` Ted Dennison
2000-01-31 0:00 ` Hyman Rosen
2000-01-31 0:00 ` Mike Silva
2000-01-31 0:00 ` Mike Silva
2000-02-01 0:00 ` Hyman Rosen
2000-02-01 0:00 ` Pat Rogers
2000-02-01 0:00 ` Hyman Rosen
2000-02-01 0:00 ` Pat Rogers
2000-02-01 0:00 ` Larry Kilgallen
2000-02-01 0:00 ` Hyman Rosen
2000-02-01 0:00 ` Pat Rogers
2000-02-01 0:00 ` Richard D Riehle
2000-02-01 0:00 ` Hyman Rosen
2000-02-02 0:00 ` Richard D Riehle
2000-02-17 0:00 ` Charles Hixson
2000-02-01 0:00 ` Larry Kilgallen
2000-02-01 0:00 ` Hyman Rosen
2000-02-02 0:00 ` Ole-Hjalmar Kristensen
2000-02-02 0:00 ` Roger Racine
2000-02-04 0:00 ` Mike Silva
2000-02-17 0:00 ` Charles Hixson
2000-02-01 0:00 ` Mike Silva
2000-02-05 0:00 ` JP Thornley
2000-02-01 0:00 ` Mike Silva
2000-02-01 0:00 ` Larry Kilgallen
2000-02-01 0:00 ` Hyman Rosen
2000-01-31 0:00 ` Hyman Rosen
2000-02-01 0:00 ` Ted Dennison
2000-02-01 0:00 ` Ole-Hjalmar Kristensen
2000-02-01 0:00 ` Hyman Rosen
2000-02-02 0:00 ` Rod Chapman [this message]
[not found] ` <m3emaug917.fsf@blight.transcend.org>
2000-02-03 0:00 ` Larry Kilgallen
2000-02-01 0:00 ` Scott Ingram
2000-02-01 0:00 ` Gautier
2000-01-31 0:00 ` Hyman Rosen
2000-02-01 0:00 ` Jean-Pierre Rosen
2000-02-01 0:00 ` Ted Dennison
2000-02-01 0:00 ` Karel Thoenissen
[not found] ` <879hjf$ggv$1@nnrp1.deja.com>
2000-02-02 0:00 ` Geography (was: JOB:Sr. SW Engineers Wanted-Fortune 500 Co) Jean-Marc Bourguet
2000-02-02 0:00 ` Karel Thoenissen
2000-02-02 0:00 ` Ted Dennison
2000-02-02 0:00 ` Gautier
2000-02-01 0:00 ` JOB:Sr. SW Engineers Wanted-Fortune 500 Co Larry Kilgallen
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox