The next research computing seminar will take place, Friday (24^th of October), 1pm-2pm.
Professor Daniel Kroening , Department of Computer Science, University of Oxford, will present a seminar entitled “Reasoning about IEEE Floating-point Arithmetic with Abstract Conflict-Driven Learning”.

Date: Friday, 24th of October 2014
Place: Wilkins Haldane Room
Time: 1:00pm – 2:00pm

Abstract:

Conflict-Driven Clause Learning is the technique that is enabling for the high performance of propositional satisfiability solvers. I will present a generalisation of Conflict-Driven Clause Learning that permits reasoning within an abstraction. I will show an exemplar, the domain of intervals over floating-point values, and its application to difficult problems in program analysis.

Speaker Bio:

Professor Daniel Kroening’s research focus is formal methods for the correct construction of hardware and software systems, with a focus on automated methods for checking compliance of an implementation with a specification. Techniques include model checking and automated testing.

He is particularly interested in applying these methods to practical hard- and software implementations given in languages like C or C++, or HDLs such as Verilog and SystemC.