Tales from Verification History
Vijay D'Silva
- 15:00 11th June 2009 ( week 7th Week, Trinity Term 2009 )Common Room (103)
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.
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.