Linear and nonlinear arithmetic in ACL2

DOI10.1007/B93958zbMATH Open1179.68136OpenAlexW219731125MaRDI QIDQ5897076FDOQ5897076

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

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

Mathematics Subject Classification ID

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

Recommendations

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

Cited in

(8)

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

Describes a project that uses

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)