Wednesday 14th August, Morning session
Martin Nyx Brain, City, University Of London
BACKGROUND:
Over the past few years there has been significant progress in the various fields of software verification resulting in many useful tools and successful deployments, both academic and commercial. However much of the work describing these tools and ideas is written by and for the research community. The scale, diversity and focus of the literature can act as a barrier, separating industrial users and the wider academic community from the tools that could make their work more efficient, more certain and more productive. This tutorial gives a simple classification of verification techniques in terms of a pyramid and uses it to describe the six main schools of verification technologies. We have found this approach valuable for building collaborations with industry as it allows us to explain the intrinsic strengths and weaknesses of techniques and pick the right tool for any given industrial application. The model also highlights some of the cultural differences and unspoken assumptions of different areas of verification and illuminates future directions.
SPEAKER:
Martin’s work is broadly within the areas of automated reasoning and automated verification for safety and security. On the automated reasoning side he mostly works on SAT / SMT solvers, including being the co-author of the SMT-LIB theory of floating-point and developing the CVC4 floating-point theory solver. In automated verification he mainly focuses on low-level and embedded software in C, C++ and Ada using a combination of abstract interpretation, symbolic execution and deductive verification and tools including SPARK and CBMC / CPROVER.