Tool Building Requirements for an API to First-Order Solvers |
| |
| Authors: | Jim Grundy, Tom Melham, Sava Krsti&#x ,Sean McLaughlin |
| |
| Affiliation: | Strategic CAD Labs, Intel Corporation, Hillsboro, OR, USA;Computing Laboratory, Oxford University, Oxford, England;Strategic CAD Labs, Intel Corporation, Hillsboro, OR, USA;School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA |
| |
| Abstract: | Effective formal verification tools require that robust implementations of automatic procedures for first-order logic and satisfiability modulo theories be integrated into expressive interactive frameworks for logical deduction, such as higher-order logic theorem provers. This paper states some pragmatic requirements for implementations of decision procedures that make them well-suited to integration into such frameworks. The aim is to open a dialogue with the designers of decision procedure software that will lead to greater and easier uptake of their implementations by verification users. |
| |
| Keywords: | abstract syntax CVC Lite decision procedure first-order logic forte higher-order logic reFLect tool integration |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
