The CProver Program Analysis Tools

Add to your list(s) Download to your calendar using vCal

• Oxford
• Tuesday 02 June 2015, 11:00-12:00
• EEE Department, Room 503.

If you have a question about this talk, please contact George A Constantinides.

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—by analysing software we can make systems safer and more efficient but to do this we need tools that can handle real world programs. This talk will present one such system, the CProver suite of analysis tools developed at University of Oxford. This gives automatic location of bugs, generation of test cases and verification for programs written in C, C++ and other languages. No knowledge of verification or theorem proving will be assumed and there will be demonstrations; all welcome.

Bio : Martin Brain is a post-doc 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. 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.

This talk is part of the CAS Talks series.

This talk is included in these lists:

• Andrea Picciau's list
• CAS Talks
• Circuits and Systems Group: Internal Seminars
• EEE Department, Room 503

Note that ex-directory lists are not shown.