This week, we’ll have a second theory seminar! Martin Brain from the University of London will come to Swansea to talk about Formal Software Verification.

There are a wide range of different approaches to the formal verification of software.  They are based on different mathematics, expressed in different terminology and have different ideas of what are important and difficult problems.  This makes it hard to compare and contrast different tools.  In this talk I will present the pyramid model of formal software verification.  It is the result of a decade of working with industrial users and gives a way of understanding how different techniques fit together and their relative strengths and weaknesses.  We will use it to understand the high-level differences between approaches and answer questions such as “How do I pick the right tool to solve my problem?” and “How can I figure out what a new tool is good for?”.