ACL2

swMATH60WikidataQ4650692MaRDI QIDQ12833

No author found.

Related Items (only showing first 100 items - show all)

An elementary linear-algebraic proof without computer-aided arguments for the group law on elliptic curves ⋮ The Imandra Automated Reasoning System (System Description) ⋮ Computer-Aided Verification for Iterative Matrix Inversion Problems in Systems and Control ⋮ A Nonstandard Functional Programming Language ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Logic Based Program Synthesis and Transformation ⋮ Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1 ⋮ Mechanical Verification of SAT Refutations with Extended Resolution ⋮ A Parallelized Theorem Prover for a Logic with Parallel Execution ⋮ Types for Proofs and Programs ⋮ Reasoning About Incompletely Defined Programs ⋮ Verification Condition Generation Via Theorem Proving ⋮ ZB 2005: Formal Specification and Development in Z and B ⋮ Binary-Compatible Verification of Filesystems with ACL2 ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Mechanizing Mathematical Reasoning ⋮ Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives ⋮ Certified Rule Labeling ⋮ Pollack-inconsistency ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm ⋮ Formalized linear algebra over Elementary Divisor Rings in Coq ⋮ Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals ⋮ Verifying Refutations with Extended Resolution ⋮ Unnamed Item ⋮ Correct Hardware Design and Verification Methods ⋮ Unnamed Item ⋮ Executing in Common Lisp, Proving in ACL2 ⋮ Transforming Programs into Recursive Functions ⋮ Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure ⋮ A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks ⋮ Extending Coq with Imperative Features and Its Application to SAT Verification ⋮ Formal Proof of a Wave Equation Resolution Scheme: The Method Error ⋮ Coverset Induction with Partiality and Subsorts: A Powerlist Case Study ⋮ Interactive Termination Proofs Using Termination Cores ⋮ A Mechanically Verified AIG-to-BDD Conversion Algorithm ⋮ Separation Logic Adapted for Proofs by Rewriting ⋮ Multi-Prover Verification of Floating-Point Programs ⋮ Automated Synthesis of Induction Axioms for Programs with Second-Order Recursion ⋮ Efficient simulation of formal processor models ⋮ On Trojan Horses of Thompson-Goerigk-Type, Their Generation, Intrusion, Detection and Prevention ⋮ Scalable Techniques for Formal Verification ⋮ Efficient execution in an automated reasoning environment ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Termination Analysis with Calling Context Graphs ⋮ Nonstandard analysis in ACL2 ⋮ Proof Assistant Decision Procedures for Formalizing Origami ⋮ A System for Computing and Reasoning in Algebraic Topology ⋮ The correctness of the fast Fourier transform: A structured proof in ACL2 ⋮ Verifying safety critical task scheduling systems in PPTL axiom system ⋮ A Sound Semantics for OCaml light ⋮ Artificial Intelligence and Symbolic Computation ⋮ Theorem Proving in Higher Order Logics ⋮ Theorem Proving in Higher Order Logics ⋮ Proceedings Seventeenth International Workshop on the ACL2 Theorem Prover and its Applications ⋮ Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications ⋮ Proceedings of the Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications ⋮ Correct Hardware Design and Verification Methods ⋮ Correct Hardware Design and Verification Methods ⋮ Theorem Proving in Higher Order Logics ⋮ Theorem Proving in Higher Order Logics ⋮ Theorem Proving in Higher Order Logics ⋮ Meta Reasoning in ACL2 ⋮ Formal Methods for Hardware Verification ⋮ Automated Deduction – CADE-19 ⋮ Formal Methods in Computer-Aided Design ⋮ Formal Methods in Computer-Aided Design ⋮ Formal Methods in Computer-Aided Design ⋮ Formal Methods in Computer-Aided Design ⋮ Mining State-Based Models from Proof Corpora ⋮ Computer Aided Verification ⋮ Algebraic Methodology and Software Technology ⋮ Verifying distributed systems ⋮ Hammering towards QED ⋮ The seventeen provers of the world. Foreword by Dana S. Scott.. ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ A heuristic prover for real inequalities ⋮ CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver ⋮ An experiment concerning mathematical proofs on computers with French undergraduate students ⋮ Proving fairness and implementation correctness of a microkernel scheduler ⋮ A formalization of powerlist algebra in ACL2 ⋮ Deadlock in packet switching networks ⋮ Directly reflective meta-programming ⋮ Ordinal arithmetic: Algorithms and mechanization ⋮ Scaling up livelock verification for network-on-chip routing algorithms ⋮ Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL ⋮ Toward automating the discovery of decreasing measures ⋮ A two-valued logic for properties of strict functional programs allowing partial functions ⋮ Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ Iterated ultrapowers for the masses ⋮ Hammer for Coq: automation for dependent type theory ⋮ The formalization of discrete Fourier transform in HOL

This page was built for software: ACL2