Name
Abstract | ||
|---|---|---|
We describe a new procedure for verifying ACL2 properties about finite state machines (FSMs) using satisfiability (SAT) solving. We present an algorithm for converting ACL2 conjectures into conjunctive normal form (CNF), which we then output and check with an external satisfiability solver. The procedure is directly available as an ACL2 proof request. When the SAT tool is successful, a theorem is added to the ACL2 system database as a lemma for use in future proof attempts. When the SAT tool is unsuccessful, we use its output to construct a counter-example to the original ACL2 property. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1145/1217975.1218001 | ACL |
Keywords | Field | DocType |
future proof attempt,finite state machine,acl2 property,sat-based procedure,acl2 system database,acl2 conjecture,sat tool,new procedure,acl2 proof request,conjunctive normal form,external satisfiability solver,satisfiability,theorem proving | Computer science,Satisfiability,Automated theorem proving,Algorithm,Finite-state machine,Theoretical computer science,Conjunctive normal form,DPLL algorithm,Solver,ACL2,Lemma (mathematics) | Conference |
ISBN | Citations | PageRank |
0-9788493-0-2 | 2 | 0.41 |
References | Authors | |
10 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Warren A. Hunt, Jr. | 1 | 520 | 59.18 |
| Erik Reeber | 2 | 86 | 5.58 |