Satisfiability solvers are static analysers
This paper shows that several propositional satisfiability algorithms compute approximations of fixed points using lattice-based abstractions. The Boolean Constraint Propagation algorithm (bcp) is a greatest fixed point computation over a lattice of partial assignments. The original algorithm of Dav...
| Հիմնական հեղինակներ: | , , |
|---|---|
| Այլ հեղինակներ: | |
| Ձևաչափ: | Conference item |
| Հրապարակվել է: |
Springer
2012
|