Tales from Verification History

Record

Program verification as a research area was born of the efforts of engineers and logicians to give meaning to programs. The fundamental ideas stem from diverse areas ranging from philosophy and linguistics to abstract algebra. In this talk, I will trace two threads in this tangled and colourful history: (1) Attempts to connect programming to logical reasoning, and (2) The drive to develop an algebra to model program behaviour. Most automated verification methods today can be viewed as combining these two approaches. This is a purely non-technical talk. The emphasis is on the evolution of ideas and more importantly, the people behind them.
[Talk Slides] and a [transcript].

Authors: D'Silva, V

• Publication date: 2009-01-01