[Eecs_bscs] REMINDER: Steve Crocker Talk Today (Fri) 2pm in ARC 221 (NEW LOCATION)

[Cribben, Denise]

Dear all,

Friendly reminder: Steve Crocker (https://en.wikipedia.org/wiki/Steve_Crocker is giving a talk today at 2pm in ARC 221 (NEW LOCATION) on the question, Why Isn't Verification Standard Practice? I encourage all of you to attend.
[https://upload.wikimedia.org/wikipedia/commons/b/b5/Steve_Crocker_%28square_crop%29.jpg]<https://en.wikipedia.org/wiki/Steve_Crocker>

Steve Crocker - Wikipedia<https://en.wikipedia.org/wiki/Steve_Crocker>
en.wikipedia.org
Stephen D. Crocker (born October 15, 1944, in Pasadena, California) is the inventor of the Request for Comments series, authoring the very first RFC and many more. He received his bachelor's degree (1968) and PhD (1977) from the University of California, Los Angeles.


What: talk by Steve Crocker entitled "Why Isn't Verification Standard Practice?"
When: Friday, April 13 at 2pm
Where: ARC 221 (NEW LOCATION)

Steve's abstract is included once again below (apologies if you've received multiple copies of this mail). I hope to see many of you there!
- Gordon

Why Isn't Verification Standard Practice?
Steve Crocker
Motivation

Despite big advances in proof systems, SMT solvers, higher order logic, etc. and some noteworthy successes in the use of formal methods in specific areas, e.g. for device drivers, formal methods are still not in common use and low-level, "simple" bugs in critical software still bedevil us. Why don't we have adequate tool support to catch those sorts of bugs before the software leaves the programmer's desk?

The purpose of this talk is to provoke discussion of the question Why Isn't Verification Standard Practice? To stimulate that discussion, I'll sketch some thoughts about how to fashion the tools. Strong arguments are welcome.
The Sketch

I think it is possible to put the pieces of this technology together in a way that achieves all of the following:


  *   Widespread, general use of formal proofs in all of the regularly used programming languages. This implies the methodology is usable and learnable.

  *   Proofs of low-level properties, particularly integrity of data structures and termination.

  *   Certainty about the proof process. The proof system should not be asked to solve unbounded or impossible problems, nor should it even have to work very hard. We need only for the proof system to see what the programmer would expect another programmer to also see, i.e. what's "obvious." The programmer should know well what the proof system is able to prove.

  *   Requires limited only annotation. As a guess, no more than 100% addition of text, and preferably less.

  *   Connected to the development environment. Most formal methods tools are separated from the development environments and run either as separate batch processes or separate interactive processes.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://listserv.ohio.edu/pipermail/eecs_bscs/attachments/20180413/540eed79/attachment.html>