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.

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Jim Grundy, Thomas F. Melham, Sava Krstic, Sean McLaughlin
• Keywords: Decision Procedure, ENTCS 2006, Expressive Interactive Frameworks, Formal Verification Tools