Abstract conflict driven learning.
Modern satisfiability solvers implement an algorithm, called Conflict Driven Clause Learning, which combines search for a model with analysis of conflicts. We show that this algorithm can be generalised to solve the lattice-theoretic problem of determining if an additive transformer on a Boolean lat...
| Autores principales: | , , |
|---|---|
| Otros Autores: | |
| Formato: | Conference item |
| Publicado: |
ACM
2013
|
| _version_ | 1826275373917143040 |
|---|---|
| author | D'Silva, V Haller, L Kroening, D |
| author2 | Giacobazzi, R |
| author_facet | Giacobazzi, R D'Silva, V Haller, L Kroening, D |
| author_sort | D'Silva, V |
| collection | OXFORD |
| description | Modern satisfiability solvers implement an algorithm, called Conflict Driven Clause Learning, which combines search for a model with analysis of conflicts. We show that this algorithm can be generalised to solve the lattice-theoretic problem of determining if an additive transformer on a Boolean lattice is always bottom. Our generalised procedure combines overapproximations of greatest fixed points with underapproximation of least fixed points to obtain more precise results than computing fixed points in isolation. We generalise implication graphs used in satisfiability solvers to derive underapproximate transformers from overapproximate ones. Our generalisation provides a new method for static analysers that operate over non-distributive lattices to reason about properties that require disjunction. © 2013 ACM. |
| first_indexed | 2024-03-06T22:57:44Z |
| format | Conference item |
| id | oxford-uuid:6102a023-3bb9-4e17-aee4-505cd29b4524 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T22:57:44Z |
| publishDate | 2013 |
| publisher | ACM |
| record_format | dspace |
| spelling | oxford-uuid:6102a023-3bb9-4e17-aee4-505cd29b45242022-03-26T17:56:50ZAbstract conflict driven learning.Conference itemhttp://purl.org/coar/resource_type/c_5794uuid:6102a023-3bb9-4e17-aee4-505cd29b4524Symplectic Elements at OxfordACM2013D'Silva, VHaller, LKroening, DGiacobazzi, RCousot, RModern satisfiability solvers implement an algorithm, called Conflict Driven Clause Learning, which combines search for a model with analysis of conflicts. We show that this algorithm can be generalised to solve the lattice-theoretic problem of determining if an additive transformer on a Boolean lattice is always bottom. Our generalised procedure combines overapproximations of greatest fixed points with underapproximation of least fixed points to obtain more precise results than computing fixed points in isolation. We generalise implication graphs used in satisfiability solvers to derive underapproximate transformers from overapproximate ones. Our generalisation provides a new method for static analysers that operate over non-distributive lattices to reason about properties that require disjunction. © 2013 ACM. |
| spellingShingle | D'Silva, V Haller, L Kroening, D Abstract conflict driven learning. |
| title | Abstract conflict driven learning. |
| title_full | Abstract conflict driven learning. |
| title_fullStr | Abstract conflict driven learning. |
| title_full_unstemmed | Abstract conflict driven learning. |
| title_short | Abstract conflict driven learning. |
| title_sort | abstract conflict driven learning |
| work_keys_str_mv | AT dsilvav abstractconflictdrivenlearning AT hallerl abstractconflictdrivenlearning AT kroeningd abstractconflictdrivenlearning |