NQTHM
From MaRDI portal
Software:19570
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