NuITP: accelerating the inductive verification of equational programs through symbolic simplification
From MaRDI portal
Cites work
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- CafeOBJ Report. The language, proof techniques, and methodologies for object-oriented algebraicspecification
- Conditional rewriting logic as a unified model of concurrency
- Coverset induction with partiality and subsorts: a powerlist case study
- DM-check: verifying invariants of concurrent systems by deductive model checking
- Extending Sledgehammer with SMT solvers
- Folding variant narrowing and optimal variant termination
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 4074541 (Why is no real title available?)
- scientific article; zbMATH DE number 3684925 (Why is no real title available?)
- scientific article; zbMATH DE number 517385 (Why is no real title available?)
- Implicit induction in conditional theories
- Induction = I-axiomatization + first-order consistency.
- Induction for SMT solvers
- Inductive reasoning with equality predicates, contextual rewriting and variant-based simplification
- Inductive Reasoning with Equality Predicates, Contextual Rewriting and Variant-Based Simplification
- Integrating Maude into Hets
- Isabelle/HOL. A proof assistant for higher-order logic
- Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
- Maude2Lean: theorem proving for Maude specifications using Lean
- Metalevel algorithms for variant satisfiability
- Narrowing based inductive proof search
- Normal forms and normal theories in conditional rewriting
- On Automation of OTS/CafeOBJ Method
- Order-Sorted Rewriting and Congruence Closure
- Program verification through characteristic formulae
- Proof by consistency
- Proofs by induction in equational theories with constructors
- Proving and rewriting
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- System description: E 1.8
- Term Rewriting and All That
- Term Rewriting and Applications
- The Lean theorem prover (system description)
- Tools and algorithms for the construction and analysis of systems. 28th international conference, TACAS 2022, held as part of the European joint conferences on theory and practice of software, ETAPS 2022, Munich, Germany, April 2--7, 2022. Proceedings. Pa
This page was built for publication: NuITP: accelerating the inductive verification of equational programs through symbolic simplification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7320678)
