[Eecs_bsee] Talk by Steve Crocker entitled "Why Isn't Verification Standard Practice?"

[Hunter, Tiffany]

-- Apologies if you receive multiple copies. ---


Hi all,

I strongly encourage you to come see a talk by Steve Crocker (https://en.wikipedia.org/wiki/Steve_Crocker) this Friday at 2pm in Stocker 326 (tentative location). Steve did his PhD work in formal methods, then later moved into networking. Abstract is below.
[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: Stocker 326 (tentative)

If you don't mind, please send me a quick note by email (gstewart at ohio.edu<mailto:gstewart at ohio.edu>) if you plan to attend -- I want to make sure we reserve an appropriately sized room (Stocker 326 currently but possibly ARC 221 if we get many responses from you and others). Note that this talk is in addition to Steve's keynote at ITS day on Thursday, April 12.

Thanks,

- 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_bsee/attachments/20180410/cc0213ae/attachment.html>