The ACL2 Sedan theorem proving system

DOI10.1007/978-3-642-19835-9_27MaRDI QIDQ3000661zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

Cites work

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

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

Describes a project that uses

Uses Software

• ACL2s
• QuickCheck
• ACL2

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)