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
Related pages
People |