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...
| المؤلفون الرئيسيون: | , , |
|---|---|
| مؤلفون آخرون: | |
| التنسيق: | Conference item |
| منشور في: |
ACM
2014
|