13 papers:
TACAS-2011-ChamarthiDMV #proving #theorem proving- The ACL2 Sedan Theorem Proving System (HRC, PCD, PM, DV), pp. 291–295.
LOPSTR-2010-HerasPR #correctness #proving #set- Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System (JH, VP, JR), pp. 37–51.
ICEIS-ISAS-2009-HidalgoGT #consistency #data type #detection #nondeterminism #performance- Efficient Data Structures for Local Inconsistency Detection in Firewall ACL Updates (SPH, RMG, FTdlR), pp. 176–181.
PPDP-2009-EastlundF #composition #induction- Making induction manifest in modular ACL2 (CE, MF), pp. 105–116.
PADL-2009-EastlundF #towards- Toward a Practical Module System for ACL2 (CE, MF), pp. 46–60.
IJCAR-2006-ReeberH #satisfiability #subclass- A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA) (ER, WAHJ), pp. 453–467.
- LOPSTR-2003-Ruiz-ReinaJHM #case study #data type #performance #reasoning
- Formal Reasoning about Efficient Data Structures: A Case Study in ACL2 (JLRR, JAAJ, MJH, FJMM), pp. 75–91.
- LOPSTR-2002-Martin-MateosAHR #framework #verification
- Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers (FJMM, JAA, MJH, JLRR), pp. 182–198.
- PADL-2002-BoyerM #thread
- Single-Threaded Objects in ACL2 (RSB, JSM), pp. 9–27.
CADE-1998-Kaufmann #verification- ACL2 Support for Verification Projects (Invited Talk) (MK), pp. 220–238.
CAV-1998-Moore #proving- An ACL2 Proof of Write Invalidate Cache Coherence (JSM), pp. 29–38.
SEKE-1996-Balmas #concept #named #programming- ACL: a Tool for Conceptual Programming (FB), pp. 198–205.
ILPS-1993-KobayashiY #concurrent #linear #logic programming #named #paradigm- ACL — A Concurrent Linear Logic Programming Paradigm (NK, AY), pp. 279–294.
