The ACL2 Sedan theorem proving system

DOI10.1007/978-3-642-19835-9_27zbMATH Open1316.68132OpenAlexW1727725625MaRDI QIDQ3000661FDOQ3000661

Authors: Harsh Raju Chamarthi, Peter C. Dillinger, Panagiotis Manolios, Daron Vroon 

Publication date: 19 May 2011

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-19835-9_27

Recommendations

• ACL2s: ``the ACL2 sedan
• An ACL2 Tutorial
• Milestones from the Pure Lisp Theorem Prover to ACL2
• Proceedings of the seventeenth international workshop on the ACL2 theorem prover and its applications, Austin, Texas, USA, May 26--27, 2022
• scientific article; zbMATH DE number 2079835

Mathematics Subject Classification ID

Cites Work

• Termination Analysis with Calling Context Graphs
• An ACL2 Tutorial
• ACL2s: ``the ACL2 sedan

Cited In (10)

• Automating Induction with an SMT Solver
• Integrating testing and interactive theorem proving
• Predicate abstraction for program verification
• Proceedings of the seventeenth international workshop on the ACL2 theorem prover and its applications, Austin, Texas, USA, May 26--27, 2022
• Integrating external deduction tools with ACL2
• The RISC ProofNavigator: a proving assistant for program verification in the classroom
• ACL2s: ``the ACL2 sedan
• Milestones from the Pure Lisp Theorem Prover to ACL2
• An ACL2 Tutorial
• Keeping logic in the trivium of computer science: a teaching perspective

Uses Software

• ACL2
• QuickCheck
• ACL2s

This page was built for publication: The ACL2 Sedan theorem proving system

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