Cited in
(only showing first 100 items - show all)- A parallelized theorem prover for a logic with parallel execution
- Inductive theorem proving based on tree grammars
- Proof assistant decision procedures for formalizing origami
- A complete proof system for propositional projection temporal logic
- The rewriting logic semantics project: a progress report
- The seventeen provers of the world. Foreword by Dana S. Scott..
- Quantitative verification of Kalman filters
- The rewriting logic semantics project: a progress report
- Verification of Year 2000 conversion rules using the ACL2 theorem prover
- Sound lemma generation for proving inductive validity of equations
- Formal proof of a wave equation resolution scheme: the method error
- Efficient execution in an automated reasoning environment
- Banishing ultrafilters from our consciousness
- Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications
- scientific article; zbMATH DE number 7552938 (Why is no real title available?)
- scientific article; zbMATH DE number 7552940 (Why is no real title available?)
- scientific article; zbMATH DE number 7552941 (Why is no real title available?)
- Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems
- All-Termination(T)
- Logic-based program synthesis and transformation. 20th international symposium, LOPSTR 2010, Hagenberg, Austria, July 23--25, 2010. Revised selected papers
- scientific article; zbMATH DE number 2090312 (Why is no real title available?)
- A formalization of the Smith normal form in higher-order logic
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
- On Trojan horses of Thompson-Goerigk-type, their generation, intrusion, detection and prevention
- On the desirability of mechanizing calculational proofs
- Proof assistance for real-time systems using an interactive theorem prover
- On the fine-structure of regular algebra
- Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability
- scientific article; zbMATH DE number 2101985 (Why is no real title available?)
- The rewriting logic semantics project
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- scientific article; zbMATH DE number 2102719 (Why is no real title available?)
- Automated and scalable verification of integer multipliers
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
- Adapting functional programs to higher order logic
- A rewriting logic approach to operational semantics
- Machines Reasoning About Machines: 2015
- Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications
- Automating Induction with an SMT Solver
- scientific article; zbMATH DE number 7552936 (Why is no real title available?)
- scientific article; zbMATH DE number 7552937 (Why is no real title available?)
- Decision Procedures for Automating Termination Proofs
- scientific article; zbMATH DE number 1863380 (Why is no real title available?)
- A formalization of powerlist algebra in ACL2
- Directly reflective meta-programming
- Automatic functional correctness proofs for functional search trees
- Formal Methods in Computer-Aided Design
- Specification and verification of concurrent programs through refinements
- The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification
- The Imandra Automated Reasoning System (System Description)
- The proof monad
- Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
- Algebraic Methodology and Software Technology
- scientific article; zbMATH DE number 2177632 (Why is no real title available?)
- Executing in Common Lisp, Proving in ACL2
- Principles of proof scores in CafeOBJ
- Expressing symmetry breaking in DRAT proofs
- Superposition with structural induction
- scientific article; zbMATH DE number 2000443 (Why is no real title available?)
- An experiment concerning mathematical proofs on computers with French undergraduate students
- A heuristic prover for real inequalities
- scientific article; zbMATH DE number 2154398 (Why is no real title available?)
- Computer Aided Verification
- Scalable Techniques for Formal Verification
- A Brief Overview of HOL4
- Analysis of meeting protocols by formalisation, simulation, and verification
- Incorporating quotation and evaluation into Church's type theory
- Function extraction
- Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks
- Proof pearl: a formal proof of Higman's lemma in ACL2
- scientific article; zbMATH DE number 2090056 (Why is no real title available?)
- Correct Hardware Design and Verification Methods
- Certified symbolic manipulation: bivariate simplicial polynomials
- A verified compiler from Isabelle/HOL to CakeML
- Toward automating the discovery of decreasing measures
- Mining state-based models from proof corpora
- Verification Condition Generation Via Theorem Proving
- A parameterized floating-point formalizaton in HOL Light
- Towards a unified theory of operational and axiomatic semantics
- Binary-Compatible Verification of Filesystems with ACL2
- From hoare logic to matching logic reachability
- A graph library for Isabelle
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Mathematical theory exploration in Theorema: reduction rings
- Meta Reasoning in ACL2
- Extending Coq with Imperative Features and Its Application to SAT Verification
- Using a first order logic to verify that some set of reals has no Lebesgue measure
- Computer theorem proving in mathematics
- Automated formal analysis and verification: an overview
- Formal Methods in Computer-Aided Design
- The rewriting logic semantics project
- Termination Analysis with Calling Context Graphs
- scientific article; zbMATH DE number 1796150 (Why is no real title available?)
- Proceedings of the seventeenth international workshop on the ACL2 theorem prover and its applications, Austin, Texas, USA, May 26--27, 2022
- scientific article; zbMATH DE number 7178359 (Why is no real title available?)
- System-level non-interference of constant-time cryptography. I: Model
- A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
- Testing-based formal verification for theorems and its application in software specification verification
This page was built for software: ACL2
