Research Computing Seminar: Reasoning about IEEE Floating-point Arithmetic with Abstract Conflict-Driven Learning

Speaker: Professor Daniel Kroening, Department of Computer Science, University of Oxford
UCL Contact: Earl Barr (Visitors from outside UCL please email in advance).
Date/Time: 24 Oct 14, 13:00 - 14:00
Venue: Haldane Room

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.

Professor Daniel Kroening