Computer-aided verification : how to trust a machine with your life

Abstract

Mathematical predictive analysis of the behaviour of circuits and computer pro- grams is a core problem in computer science. Research in formal verification and semantics of programming languages has been an active field for a number of decades, but it was only through techniques developed over these past twenty years that they have been scaled up to work on non-trivial case-studies. This report gives an overview of a number of computer- aided formal verification areas I have been working on over these past couple of years in such a way to be accessible to computer scientists in other disciplines. Brief mention is made of problems in these areas I am actively working on. It does not purport to be an overview of the whole field of computer-aided formal verification or a detailed technical account of my research.