Linear and nonlinear arithmetic in ACL2

DOI10.1007/B93958zbMATH Open1179.68136OpenAlexW219731125MaRDI QIDQ5897076FDOQ5897076

J Strother Moore, Robert Bellarmine Krug, Warren A. jun. Hunt

Publication date: 5 February 2010

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/b93958

Recommendations

• An ACL2 Tutorial
• Theory extension in ACL2(r)
• Nonstandard analysis in ACL2
• Toward verifying nonlinear integer arithmetic
• Solving non-linear arithmetic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (6)

• Real World Verification
• A heuristic prover for real inequalities
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic
• Formalization of Bernstein polynomials and applications to global optimization
• Nonstandard analysis in ACL2

Uses Software

• ACL2

This page was built for publication: Linear and nonlinear arithmetic in ACL2

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5897076)