COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > 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 - 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.
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.
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
- Computer Laboratory talks
- Computing and Mathematics
- 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. |
## Other listsInterdisciplinary Design: Debates and Seminars Modelling Biology Communications Research Group Seminar## Other talksHow to rediscover a medical secret in eighteenth-century France: the lost recipe of the Chevalier de Guiller's powder febrifuge Roland the Hero Stokes-Smoluchowski-Einstein-Langevin theory for active colloidal suspensions A compositional approach to scalable statistical modelling and computation Mechanical performance of wall structures in 3D printing processes: theory, design tools and experiments Frontiers in paediatric cancer research |