swMATH7543MaRDI QIDQ19570FDOQ19570
Author name not available (Why is that?)
Official website: http://www.cs.utexas.edu/users/boyer/ftp/nqthm/
Cited In (only showing first 100 items - show all)
- 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
- Automatic derivation of the irrationality of \(e\)
- Mechanizing structural induction. II: Strategies
- Simulation Refinement for Concurrency Verification
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- Verifying a signature architecture: a comparative case study
- Simulation refinement for concurrency verification
- Term rewriting and beyond -- theorem proving in Isabelle
- Theories for mechanical proofs of imperative programs
- Specification and verification of concurrent programs through refinements
- A formalization of powerlist algebra in ACL2
- Analysis of a biphase mark protocol with Uppaal and PVS
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Title not available (Why is that?)
- Programmed strategies for program verification
- The verified incremental design of a distributed spanning tree algorithm: Extended abstract
- A framework for the verification of certifying computations
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
- A verification system for concurrent programs based on the Boyer-Moore prover
- Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks
- A Ramsey theorem in Boyer-Moore logic
- An integrated approach to high integrity software verification
- Mathematical induction in Otter-lambda
- Toward automating the discovery of decreasing measures
- Verification of the Miller-Rabin probabilistic primality test.
- Efficient second-order matching
- Superposition theorem proving for abelian groups represented as integer modules
- Mechanizing structural induction. I: Formal system
- A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7™ Processor
- On Shostak's decision procedure for combinations of theories
- A functional formalization of on chip communications
- 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
- On proving the termination of algorithms by machine
- A formalization of the Knuth-Bendix(-Huet) critical pair theorem
- Hybrid interactive theorem proving using Nuprl and HOL
- ACL2s: ``the ACL2 sedan
- Wait-free concurrent memory management by create and read until deletion (CaRuD)
- Combining theories with shared set operations
- Mechanical verification on strategies
- A verified common lisp implementation of Buchberger's algorithm in ACL2
- Fermat, Euler, Wilson -- three case studies in number theory
- An assertional proof for a construction of an atomic variable
- Operating system verification---an overview
- Proof assistants: history, ideas and future
- Context induction: A proof principle for behavioural abstractions and algebraic implementations
- Introduction to the OBDD algorithm for the ATP community
- A mechanically verified incremental garbage collector
- Ordinal arithmetic: Algorithms and mechanization
- A PVS theory for term rewriting systems
- An ACL2 Tutorial
- Algebraic models of microprocessors architecture and organisation
- A semi-algorithm for algebraic implementation proofs
- Title not available (Why is that?)
- Induction using term orderings
- A mechanical analysis of program verification strategies
- Mechanically certifying formula-based Noetherian induction reasoning
- Proving Matijasevich's lemma with a default arithmetic strategy
- The automated proof of a trace transformation for a bitonic sort
- Bottom-up evaluation of Datalog programs with arithmetic constraints
- Middle-out reasoning for synthesis and induction
- Using hints to increase the effectiveness of an automated reasoning program: Case studies
- IsaCoSy
- Theorem proving in cancellative abelian monoids (extended abstract)
- Orderings for term-rewriting systems
- Using induction and rewriting to verify and complete parameterized specifications
- Title not available (Why is that?)
- Title not available (Why is that?)
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Rewriting with equivalence relations in ACL2
- The addition of bounded quantification and partial functions to a computational logic and its theorem prover
- Automata-driven automated induction
- Foundations of a theorem prover for functional and mathematical uses
- Set theory for verification. I: From foundations to functions
- Specification and proof in membership equational logic
- Structured theory development for a mechanized logic
- ML
- Superposition theorem proving for abelian groups represented as integer modules
- QingTing1
- UCLID
- HOL
- Nuprl
- AURA
- LISP
- SPIKE
- ACL2s
- HipSpec
- Zeno
- MathXpert
- LCF
- GC
- Jerusat
- LEGO
- SAD
- Milawa
- SbReve2
This page was built for software: NQTHM
