NQTHM

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