An Introduction to Automatic Software Verification and CPROVER

Time: 14.00

Venue: Kilburn, L.T.1.4, The University of Manchester

Sorry, this event has now ended.

Abstract : Modern technology is increasingly reliant on software, even in `safety critical' domains where software faults can cause loss of life or major damage. This is both a challenge and an opportunity for the academic field of computer science -- formal analysis of software can make systems safer, more secure and more efficient but to achieve this, the analysis technology must be accessible and cost-efficient for systems creators to use. This talk introduces automatic software verification (what, who, why and how), presents the CPROVER framework and summarises a decade of experience in applying these tools in industry. No knowledge of verification or theorem proving will be assumed; all welcome!

Bio : Martin Nyx Brain is project lead for the ASVAT project and a researcher in the automatic verification group of the University of Oxford. As part of the CPROVER team, he focuses on using automatic theorem provers (such as SAT and SMT solvers) to analyse C and other low level software to generate test cases, find bugs and prove safety
and security. Particular areas of expertise include numerical and floating-point programs (for control or data processing), the use of abstractions in reasoning and supporting industrial users in integrating verification research into their tools and services. He is a co-author of the SMT-LIB theory of floating point and a CVC4 developer. Also he still finds "writing about myself in the third person" jokes in biographies funny.