Model-checking: from real life to mathematics

Julian Bradfield


"Model-checking" is a popular and highly successful technique for performing formal verification of both hardware and software systems. It relies on a range of theories and techniques from theoretical computer science and logic: temporal logics are used to express the properties to be checked, process algebras may be used to express the systems under examination, automata theory is used to produce algorithms for model-checking, and so on. Moreover, the study of techniques inspired by the very practical demands of model-checking, can lead into mathematical questions that most people would consider very theoretical -- even by mathematicians' standards, let alone computer scientists'. In this talk, I will give a high-level overview of model-checking and related areas: what the problem is (verification), how we can formalize it (logic and automata), how we can then solve it (model-checking itself), and a glimpse at some of the related mathematical topics (game theory, descriptive set theory).
Tuesday 19th February 2002, 14:00
Robert Recorde Room
Department of Computer Science