ACL2s: ``the ACL2 sedan

DOI10.1016/J.ENTCS.2006.09.018MaRDI QIDQ2867932zbMATH OpenOpenAlexFDO

Authors Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J Strother Moore

Publication date 20 December 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2006.09.018

zbMATH Keywords

theorem provingACL2Eclipsescript management

Mathematics Subject Classification ID

Recommendations

• The ACL2 Sedan theorem proving system
• An ACL2 Tutorial
• Proceedings of the seventeenth international workshop on the ACL2 theorem prover and its applications, Austin, Texas, USA, May 26--27, 2022
• Milestones from the Pure Lisp Theorem Prover to ACL2
• Structured theory development for a mechanized logic

Cites work

• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• ACL2s: ``the ACL2 sedan
• An ACL2 Tutorial
• Termination Analysis with Calling Context Graphs
• The size-change principle for program termination

Cited in

(10)

• All-Termination(T)
• Delay-bounded scheduling without delay!
• Integrating testing and interactive theorem proving
• ACL2(ml): machine-learning for ACL2
• Proceedings of the seventeenth international workshop on the ACL2 theorem prover and its applications, Austin, Texas, USA, May 26--27, 2022
• Testing-based formal verification for theorems and its application in software specification verification
• Integrating external deduction tools with ACL2
• ACL2s: ``the ACL2 sedan
• An ACL2 Tutorial
• The ACL2 Sedan theorem proving system

Describes a project that uses

Uses Software

• DrACuLa
• ACL2s
• NQTHM
• Proof General
• DrScheme
• ACL2

This page was built for publication: ACL2s: ``the ACL2 sedan

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