ACL2s: ``the ACL2 sedan

DOI10.1016/J.ENTCS.2006.09.018zbMATH Open1278.68258OpenAlexW2145365771MaRDI QIDQ2867932FDOQ2867932

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

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

zbMATH Keywords

theorem provingACL2Eclipsescript management

Mathematics Subject Classification ID

Cites Work

• The size-change principle for program termination
• Title not available (Why is that?)
• Termination Analysis with Calling Context Graphs
• An ACL2 Tutorial
• ACL2s: ``the ACL2 sedan

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

Uses Software

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

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)