Sciweavers

Share
ENTCS
2006

Tool Building Requirements for an API to First-Order Solvers

3 years 7 months ago
Tool Building Requirements for an API to First-Order Solvers
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.
Jim Grundy, Thomas F. Melham, Sava Krstic, Sean Mc
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Jim Grundy, Thomas F. Melham, Sava Krstic, Sean McLaughlin
Comments (0)
books