Abstract Satisfaction
This article introduces an abstract interpretation framework that codifies the operations in SAT and SMT solvers in terms of lattices, transformers and fixed points. We develop the idea that a formula denotes a set of models in a universe of structures. This set of models has characterizations as fi...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Conference item |
| Published: |
ACM
2014
|