The following pages link to ACL2 (Q12833):
Displayed 50 items.
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- A heuristic prover for real inequalities (Q287379) (← links)
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (Q333325) (← links)
- A two-valued logic for properties of strict functional programs allowing partial functions (Q352946) (← links)
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- On the role of formalization in computational mathematics (Q372699) (← links)
- Proceedings of the 7th workshop on user interfaces for theorem provers (UITP 2006), Seattle, WA, USA, August 21, 2006 (Q373628) (← links)
- A complete proof system for propositional projection temporal logic (Q391223) (← links)
- The rewriting logic semantics project: a progress report (Q393080) (← links)
- Function extraction (Q436372) (← links)
- Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks (Q437040) (← links)
- Proof pearl: a formal proof of Higman's lemma in ACL2 (Q438550) (← links)
- Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning (Q457250) (← links)
- Certifying algorithms (Q465678) (← links)
- Automatic verification of reduction techniques in higher order logic (Q469363) (← links)
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- Logic-based program synthesis and transformation. 20th international symposium, LOPSTR 2010, Hagenberg, Austria, July 23--25, 2010. Revised selected papers (Q532632) (← links)
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4 (Q540690) (← links)
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem (Q616850) (← links)
- Trace-based verification of imperative programs with I/O (Q617977) (← links)
- Reasoning about memory layouts (Q633298) (← links)
- Certifying compilers using higher-order theorem provers as certificate checkers (Q633302) (← links)
- Computer theorem proving in mathematics (Q704001) (← links)
- A formal proof of the deadline driven scheduler in PPTL axiomatic system (Q744103) (← links)
- Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (Q779625) (← links)
- Formal verification of the VAMP floating point unit (Q816201) (← links)
- Formalization of fixed-point arithmetic in HOL (Q816219) (← links)
- The seventeen provers of the world. Foreword by Dana S. Scott.. (Q819987) (← links)
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver (Q832260) (← links)
- Proving fairness and implementation correctness of a microkernel scheduler (Q835766) (← links)
- A formalization of powerlist algebra in ACL2 (Q846164) (← links)
- Directly reflective meta-programming (Q848742) (← links)
- Ordinal arithmetic: Algorithms and mechanization (Q851144) (← links)
- Toward automating the discovery of decreasing measures (Q861690) (← links)
- The rewriting logic semantics project (Q877024) (← links)
- Formal correctness of a quadratic unification algorithm (Q877825) (← links)
- A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures (Q877828) (← links)
- A complete axiom system for propositional projection temporal logic with cylinder computation model (Q896162) (← links)
- Rewriting with equivalence relations in ACL2 (Q928668) (← links)
- A mechanical analysis of program verification strategies (Q928673) (← links)
- A functional formalization of on chip communications (Q931433) (← links)
- The higher-order-logic Formath (Q935562) (← links)
- Inference rules for proving the equivalence of recursive procedures (Q938300) (← links)
- Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings (Q955386) (← links)
- Partial and nested recursive function definitions in higher-order logic (Q972425) (← links)
- The proof monad (Q974136) (← links)
- Integrating external deduction tools with ACL2 (Q1006728) (← links)
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- A rewriting logic approach to operational semantics (Q1012130) (← links)
- Certifying properties of an efficient functional program for computing Gröbner bases (Q1012152) (← links)