University of Oxford Logo University of OxfordDepartment of Computer Science - Home
Linked in
Linked in
Follow us on twitter
Twitter
On Facebook
Facebook
Instagram
Instagram

Abstract Conflict Driven Learning

V. D'Silva‚ L. Haller and D. Kroening

Abstract

We lift the conflict driven clause learning algorithm used by modern satisfiability solvers to a lattice-theoretic problem of determining if a distributive transformer on a Boolean lattice is always bottom. Our lifting enables static analyzers to reason about properties that require disjunction by operating over non-distributive lattices. The new procedure combines overapproximations of greatest fixed points with underapproximation of least fixed points to obtain more precise results than either iteration in isolation. We generalise implication graphs in propositional solvers to a general technique for constructing underapproximate transformers in overapproximate domains. Our procedure is based on a characterisation of model search and conflict analysis in propositional solvers as fixed point iteration in abstract domains.

Details

Book Title

POPL

Year

2013

Links

BibTeX

Related pages

People