The following pages link to ACL2 (Q12833):
Displayed 50 items.
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Implementing and reasoning about hash-consed data structures in Coq (Q2351422) (← links)
- Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets (Q2352482) (← links)
- On the fine-structure of regular algebra (Q2352506) (← links)
- Formalization of transform methods using HOL Light (Q2364690) (← links)
- Agent-oriented modeling of the dynamics of biological organisms (Q2383958) (← links)
- Satisfiability modulo bounded checking (Q2405244) (← links)
- Efficient certified RAT verification (Q2405252) (← links)
- System-level non-interference of constant-time cryptography. I: Model (Q2417947) (← links)
- Verifying a scheduling protocol of safety-critical systems (Q2424721) (← links)
- Tools and algorithms for the construction and analysis of systems. 17th international conference, TACAS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 -- April 3, 2011. (Q2431632) (← links)
- Analysis of meeting protocols by formalisation, simulation, and verification (Q2463822) (← links)
- Programs from proofs using classical dependent choice (Q2482844) (← links)
- Translation of resolution proofs into short first-order proofs without choice axioms (Q2486578) (← links)
- Systems specification by basic protocols (Q2508786) (← links)
- A parameterized floating-point formalizaton in HOL Light (Q2520685) (← links)
- Formal verification of a generic framework to synthesize SAT-provers (Q2583288) (← links)
- Theory extension in ACL2(r) (Q2642461) (← links)
- Code-carrying theories (Q2643124) (← links)
- Construction and analysis of ground models and their refinements as a foundation for validating computer-based systems (Q2643128) (← links)
- Computer assisted reasoning. A Festschrift for Michael J. C. Gordon (Q2655321) (← links)
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (Q2655326) (← links)
- (Q2723435) (← links)
- (Q2734602) (← links)
- Mathematical Theory Exploration in Theorema: Reduction Rings (Q2817288) (← links)
- Testing-Based Formal Verification for Theorems and Its Application in Software Specification Verification (Q2827442) (← links)
- Automatic Functional Correctness Proofs for Functional Search Trees (Q2829265) (← links)
- Mechanical Software Verification (Q2841237) (← links)
- Ours Is to Reason Why (Q2842639) (← links)
- (Q2852038) (← links)
- (Q2852094) (← links)
- ACL2s: “The ACL2 Sedan” (Q2867932) (← links)
- Proof-Pattern Recognition and Lemma Discovery in ACL2 (Q2870142) (← links)
- Automated formal analysis and verification: an overview (Q2871577) (← links)
- A Rewriting Logic Approach to Operational Semantics (Extended Abstract) (Q2871834) (← links)
- Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete (Q2879266) (← links)
- The Reflective Milawa Theorem Prover Is Sound (Q2879267) (← links)
- Rough Diamond: An Extension of Equivalence-Based Rewriting (Q2879275) (← links)
- Mechanical Certification of Loop Pipelining Transformations: A Preview (Q2879278) (← links)
- Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs (Q2891399) (← links)
- Automating Induction with an SMT Solver (Q2891425) (← links)
- A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers (Q2914732) (← links)
- (Q2917406) (← links)
- An Axiomatization for Cylinder Computation Model (Q2920446) (← links)
- Certified symbolic manipulation (Q2963240) (← links)
- Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
- (Q2985126) (← links)
- The ACL2 Sedan Theorem Proving System (Q3000661) (← links)
- Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System (Q3003483) (← links)
- (Q3021914) (← links)