NQTHM

swMATH7543MaRDI QIDQ19570FDOQ19570

Author name not available (Why is that?)

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
• 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
• Wait-free concurrent memory management by Create and Read until Deletion (CaRuD)
• Theories for mechanical proofs of imperative programs
• Hybrid interactive theorem proving using nuprl and HOL
• 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
• 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?)
• A framework for the verification of certifying computations
• 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 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.
• Title not available (Why is that?)
• Superposition theorem proving for abelian groups represented as integer modules
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• 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
• A functional formalization of on chip communications
• A PVS Theory for Term Rewriting Systems
• Rewriting with equivalence relations in ACL2
• 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
• 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
• On proving the termination of algorithms by machine
• A formalization of the Knuth-Bendix(-Huet) critical pair theorem
• Specification and proof in membership equational logic
• ACL2s: ``the ACL2 sedan
• Structured theory development for a mechanized logic
• Superposition theorem proving for abelian groups represented as integer modules
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Mechanical verification on strategies
• Fermat, Euler, Wilson -- three case studies in number theory
• An assertional proof for a construction of an atomic variable
• Operating system verification---an overview
• Context induction: A proof principle for behavioural abstractions and algebraic implementations
• SAD as a mathematical assistant -- how should we go from here to there?
• Shallow confluence of conditional term rewriting systems
• Introduction to the OBDD algorithm for the ATP community
• A mechanically verified incremental garbage collector
• Ordinal arithmetic: Algorithms and mechanization
• An ACL2 Tutorial
• An even closer integration of linear arithmetic into inductive theorem proving
• Title not available (Why is that?)
• Induction using term orderings
• IMPS: An interactive mathematical proof system
• Partial and nested recursive function definitions in higher-order logic
• An overview of the Tecton proof system
• Mechanically certifying formula-based Noetherian induction reasoning
• Proving Matijasevich's lemma with a default arithmetic strategy
• A Verified Runtime for a Verified Theorem Prover
• Proving theorems by reuse
• 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
• Combining Theories with Shared Set Operations
• New uses of linear arithmetic in automated theorem proving by induction
• Wait-free linearization with a mechanical proof
• A temporal logic for real-time partial ordering with named transactions
• Title not available (Why is that?)
• Cancellative Abelian monoids and related structures in refutational theorem proving. I
• Automatic derivation of the irrationality of \(e\)
• Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs
• A taxonomy of exact methods for partial Max-SAT
• Constraint contextual rewriting.
• An experiment with the Boyer-Moore theorem prover: A proof of Wilson's theorem
• The automation of proof: a historical and sociological exploration
• Induction using term orders
• Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto
• An automatic proof of Gödel's incompleteness theorem
• Programmed strategies for program verification
• Nonconstructive computational mathematics
• Verification by Parallelization of Parametric Code
• The verified incremental design of a distributed spanning tree algorithm: Extended abstract
• Incorporating quotation and evaluation into Church's type theory
• A verification system for concurrent programs based on the Boyer-Moore prover
• Efficient second-order matching
• Abstraction of hardware construction
• INDUCTIVE COMPOSITION OF NUMBERS WITH MAXIMUM, MINIMUM, AND ADDITION: A New Theory for Program Execution-Time Analysis

This page was built for software: NQTHM