University of Cambridge > > Logic and Semantics Seminar (Computer Laboratory) > Why Isn’t Verification Standard Practice?

Why Isn’t Verification Standard Practice?

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

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


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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity