X Close

Research Software Development


Reliability, readability, and efficiency in scientific software


Archive for October, 2014

Research Computing Seminar

Susanne Claus21 October 2014

The next research computing seminar will take place, Friday (24th 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


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.