Designing programs to check their work (abstract)

ABSTRACT

Designing Programs to Check Their Work Professor Manuel Blurn Department of EECS UC Berkeley and International Computer Science Institute Berkeley, California Abstract Students, engineers, programmers... are all expected to check their work. Computer programs are not. There are several reasons for this: 1. Computer hardware almost never makes errors -- but that fails to recognize that programmers do! 2. Programs are hard enough to write without having to also write program checkers for them -- but that is the price of increased confidence! 3. There is no clear notion what constitutes a good checker. Indeed, the same students and engi-neers who are cautioned to check their work are rarely informed what it is that makes a proce-dure good for doing so -- but that is just the sort of problem that computer science should be able to solve! In my view, the lack of correctness checks in programs is an oversight. Programs have bugs that could perfectly well be caught by such checks. This talk urges that programs be written to check their work, and outlines a promising and rigorous approach to the study of this fascinating new area.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

General Terms:
Design, Verification