Name
Title | ||
|---|---|---|
A SAT-based decision procedure for the subclass of unrollable list formulas in ACL2 (SULFA) |
Abstract | ||
|---|---|---|
We define the Subclass of Unrollable List Formulas in ACL2 (SULFA). SULFA is a subclass of ACL2 formulas based on list structures that is sufficiently expressive to include invariants of finite state machines (FSMs). We have extended the ACL2 theorem prover to include a new proof mechanism, which can recognize SULFA formulas and automatically verify them with a SAT-based decision procedure. When this decision procedure is successful, a theorem is added to the ACL2 system database as a lemma for use in future proof attempts. When unsuccessful, a counter-example to the SULFA property is presented. We are using SULFA and its SAT-based decision procedure as part of a larger system to verify components of the TRIPS processor. Our verification system translates Verilog designs automatically into ACL2 models. These models are written such that their invariants are SULFA properties, which can be verified by our SAT-based decision procedure, traditional theorem proving, or a mixture of the two. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1007/11814771_38 | IJCAR |
Keywords | Field | DocType |
traditional theorem,acl2 formula,decision procedure,unrollable list formula,acl2 theorem prover,sulfa property,acl2 system database,acl2 model,sat-based decision procedure,larger system,sulfa formula,finite state machine,theorem prover,theorem proving | Constraint satisfaction,Discrete mathematics,Computer science,Automated theorem proving,Propositional calculus,Proof theory,Algorithm,Finite-state machine,Conjunctive normal form,ACL2,Lemma (mathematics) | Conference |
Volume | ISSN | ISBN |
4130 | 0302-9743 | 3-540-37187-7 |
Citations | PageRank | References |
8 | 0.70 | 10 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Erik Reeber | 1 | 86 | 5.58 |
| Warren A. Hunt | 2 | 230 | 13.86 |