BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Why Isn’t Verification Standard Practice? - Steve Crocker\, ICAN
 N
DTSTART:20140701T130000Z
DTEND:20140701T140000Z
UID:TALK53326@talks.cam.ac.uk
CONTACT:Jonathan Hayman
DESCRIPTION:_Motivation_\n\nDespite big advances in proof systems\, SMT so
 lvers\, higher order logic\, etc. and some noteworthy successes in the use
  of formal methods in specific areas\, e.g. for device drivers\, formal me
 thods are still not in common user and low-level\, “simple” bugs in cr
 itical software still bedevils us.  Why don’t we have adequate tool supp
 ort to catch those sorts of bugs before the software leaves the programmer
 ’s desk?\n\nThe purpose of this talk is to provoke discussion of the que
 stion Why Isn’t Verification Standard Practice?  To stimulate that discu
 ssion\, I’ll sketch some thoughts about how to fashion the tools.  Stron
 g arguments are welcome.\n\n\n_The Sketch_\n\nI think it is possible to pu
 t the pieces of this technology together in a way that achieves all of the
  following:\n\n* Widespread\, general use of formal proofs in all of the r
 egularly used programming languages.  This implies the methodology is usab
 le and learnable.\n\n* Proofs of low-level properties\, particularly integ
 rity of data structures and termination.\n\n* Certainty about the proof pr
 ocess.  The proof system should not be asked to solve unbounded or impossi
 ble problems\, nor should it even have to work very hard.  We only need fo
 r the proof system to see what the programmer would expect another program
 mer to also see\, i.e. what’s “obvious.”  The programmer should know
  well what the proof system is able to prove.\n\n* Requires limited only a
 nnotation.  As a guess\, no more than 100% addition of text\, and preferab
 ly less.\n\n* Connected to the development environment.  Most formal metho
 ds tools are separated from the development environments and run either as
  separate batch processes or separate interactive processes.\n
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR