NQTHM
From MaRDI portal
Cited in
(only showing first 100 items - show all)- An ordinal measure based procedure for termination of functions
- New uses of linear arithmetic in automated theorem proving by induction
- Deductive and inductive synthesis of equational programs
- On the comparison of HOL and Boyer-Moore for formal hardware verification
- An extension of the Boyer-Moore theorem prover to support first-order quantification
- A proof of the nonrestoring division algorithm and its implementation on an ALU
- A temporal logic for real-time partial ordering with named transactions
- Wait-free linearization with a mechanical proof
- Cancellative Abelian monoids and related structures in refutational theorem proving. I
- scientific article; zbMATH DE number 4033137 (Why is no real title available?)
- Mechanizing structural induction. II: Strategies
- Automatic derivation of the irrationality of \(e\)
- A taxonomy of exact methods for partial Max-SAT
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- Learning strategies for mechanised building of decision procedures
- Simulation Refinement for Concurrency Verification
- Simulation refinement for concurrency verification
- Verifying a signature architecture: a comparative case study
- Term rewriting and beyond -- theorem proving in Isabelle
- Deductive verification of advanced out-of-order microprocessors.
- Constraint contextual rewriting.
- Theories for mechanical proofs of imperative programs
- A formalization of powerlist algebra in ACL2
- Analysis of a biphase mark protocol with Uppaal and PVS
- An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
- Specification and verification of concurrent programs through refinements
- Orderings for term-rewriting systems
- Induction using term orders
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- The automation of proof: a historical and sociological exploration
- Theorem proving in cancellative abelian monoids (extended abstract)
- Using induction and rewriting to verify and complete parameterized specifications
- Deduction as an engineering science
- scientific article; zbMATH DE number 4164171 (Why is no real title available?)
- Nonconstructive computational mathematics
- Programmed strategies for program verification
- scientific article; zbMATH DE number 193479 (Why is no real title available?)
- An automatic proof of Gödel's incompleteness theorem
- The verified incremental design of a distributed spanning tree algorithm: Extended abstract
- A framework for the verification of certifying computations
- Incorporating quotation and evaluation into Church's type theory
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
- Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks
- A verification system for concurrent programs based on the Boyer-Moore prover
- Verification by Parallelization of Parametric Code
- An integrated approach to high integrity software verification
- Mathematical induction in Otter-lambda
- Toward automating the discovery of decreasing measures
- A Ramsey theorem in Boyer-Moore logic
- Verification of the Miller-Rabin probabilistic primality test.
- Superposition theorem proving for abelian groups represented as integer modules
- scientific article; zbMATH DE number 1209602 (Why is no real title available?)
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Mechanizing structural induction. I: Formal system
- Abstraction of hardware construction
- Efficient second-order matching
- INDUCTIVE COMPOSITION OF NUMBERS WITH MAXIMUM, MINIMUM, AND ADDITION: A New Theory for Program Execution-Time Analysis
- Bounded delay for a free address
- Circuits as streams in Coq: verification of a sequential multiplier
- A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
- A functional formalization of on chip communications
- Rewriting with equivalence relations in ACL2
- On Shostak's decision procedure for combinations of theories
- Using eternity variables to specify and prove a serializable database interface
- A framework for verifying bit-level pipelined machines based on automated deduction and decision procedures
- N. G. de Bruijn's contribution to the formalization of mathematics
- Proof movie -- a proof with the Boyer-Moore prover
- Convergence: integrating termination and abort-freedom
- Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem
- The addition of bounded quantification and partial functions to a computational logic and its theorem prover
- Lazy techniques for fully expansive theorem proving
- Automata-driven automated induction
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem
- Set theory for verification. I: From foundations to functions
- ACL2
- ML
- LARCH
- PREVAIL
- VLISP
- OMRS
- PVS
- QingTing1
- UCLID
- HOL
- Nuprl
- AURA
- LISP
- On proving the termination of algorithms by machine
- SPIKE
- ACL2s
- HipSpec
- Zeno
- MathXpert
- LCF
- GC
- Jerusat
- LEGO
- SAD
- Milawa
This page was built for software: NQTHM
