Why Isn’t Verification Standard Practice?

Add to your list(s) Download to your calendar using vCal

• Steve Crocker, ICANN
• Tuesday 01 July 2014, 14:00-15:00
• Room FW26, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Jonathan Hayman.

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 user and low-level, “simple” bugs in critical software still bedevils 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 only need 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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.