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...
| Principais autores: | , , |
|---|---|
| Outros Autores: | |
| Formato: | Conference item |
| Publicado em: |
ACM
2014
|