Extending ACL2 with SMT Solvers
The work
| Authors | Yan Peng; Mark Greenstreet |
|---|---|
| Editors | |
| Type | article |
| Year | 2015 |
| Citekey | peng2015extending |
Where it appeared
| Published in | Electronic Proceedings in Theoretical Computer Science |
|---|---|
| Publisher | Open Publishing Association |
| Volume | 192 |
| Pages | 61--77 |
Identifiers
| arXiv | 1509.06082 |
|---|---|
| DOI | 10.4204/eptcs.192.6 |
| ISSN | 2075-2180 |
Access
| Landing page | https://doi.org/10.4204/eptcs.192.6 |
|---|
Related
| Distinct from | biere1999symbolic |
|---|---|
| Distinct from | bloem2018formal |
| Distinct from | dhingra1987formal |
| Distinct from | ferres2023electrical |
| Distinct from | lee2026formal |
| Distinct from | manjrekar2025automating |
| Distinct from | oulkaid2026modeling |
| Distinct from | yan2010formal |
| Distinct from | yan2012oscillator |
From crossref.
Abstract
We present our extension of ACL2 with Satisfiability Modulo Theories (SMT) solvers using ACL2’s trusted clause processor mechanism. We are particularly interested in the verification of physical systems including Analog and Mixed-Signal (AMS) designs. ACL2 offers strong induction abilities for reasoning about sequences and SMT complements deduction methods like ACL2 with fast nonlinear arithmetic solving procedures. While SAT solvers have been integrated into ACL2 in previous work, SMT methods raise new issues because of their support for a broader range of domains including real numbers and uninterpreted functions. This paper presents Smtlink, our clause processor for integrating SMT solvers into ACL2. We describe key design and implementation issues and describe our experience with its use.
A copy is held
pdf, 213.6 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via crossref |
|---|---|
| Added | 2026-09-16 02:05 UTC |
| Approved by | a person 2026-10-02 10:03 UTC |
Filed under
Cite it as
@article{peng2015extending,
title = {Extending ACL2 with SMT Solvers},
author = {Yan Peng and Mark Greenstreet},
year = {2015},
journal = {Electronic Proceedings in Theoretical Computer Science},
publisher = {Open Publishing Association},
volume = {192},
pages = {61--77},
issn = {2075-2180},
eprint = {1509.06082},
doi = {10.4204/eptcs.192.6},
}
This record lives at https://refs.drheap.org/peng2015extending/ and will keep doing so.