ACL2s: “The ACL2 Sedan”

DOI10.1016/j.entcs.2006.09.018zbMath1278.68258OpenAlexW2145365771MaRDI QIDQ2867932

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

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

Related Items

Delay-bounded scheduling without delay! ⋮ An ACL2 Tutorial ⋮ The ACL2 Sedan Theorem Proving System ⋮ All-Termination(T) ⋮ Testing-Based Formal Verification for Theorems and Its Application in Software Specification Verification ⋮ ACL2s: “The ACL2 Sedan”

Uses Software

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

Cites Work

• Unnamed Item
• ACL2s: “The ACL2 Sedan”
• An ACL2 Tutorial
• The size-change principle for program termination
• Termination Analysis with Calling Context Graphs