Name
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. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1016/j.entcs.2005.12.003 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
abstract syntax,decision procedure software,logical deduction,cvc lite,decision procedure,expressive interactive framework,tool building requirements,forte,t ool integration,tool integration,easier uptake,automatic procedure,effective formal verification tool,higher-order logic,first-order solvers,refl ect,higher-order logic theorem provers,verification user,first-order logic,reflect,theorem prover,first order,formal verification,satisfiability modulo theories,first order logic,higher order logic | Discrete mathematics,Programming language,Computer science,Implementation,Theoretical computer science,First-order logic,Software,Deductive reasoning,Abstract syntax,Higher-order logic,Satisfiability modulo theories,Formal verification | Journal |
Volume | Issue | ISSN |
144 | 2 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
4 | 0.52 | 10 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jim Grundy | 1 | 179 | 18.11 |
| Thomas F. Melham | 2 | 384 | 35.63 |
| Sava Krstić | 3 | 144 | 9.41 |
| Sean McLaughlin | 4 | 140 | 9.39 |