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: | , , |
|---|---|
| 其他作者: | |
| 格式: | Conference item |
| 出版: |
ACM
2014
|