Using induction and rewriting to verify and complete parameterized specifications

DOI10.1016/S0304-3975(96)80708-0zbMath0874.68198OpenAlexW4246703498MaRDI QIDQ672051

Adel Bouhoula

Publication date: 27 February 1997

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0304-3975(96)80708-0

zbMATH Keywords

Term rewriting systemsTheorem provingImplicit inductionParameterized conditional specificationsspecification and validation of softwareSufficient completeness

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Order-Sorted Parameterization and Induction, Sufficient completeness verification for conditional and constrained TRS, Specification and proof in membership equational logic, Mechanically certifying formula-based Noetherian induction reasoning, Proving weak properties of rewriting, A general framework to build contextual cover set induction provers, Automata-driven automated induction

Uses Software

• NQTHM

Cites Work

• Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
• Testing for the ground (co-)reducibility property in term-rewriting systems
• Rippling: A heuristic for guiding inductive proofs
• Proofs by induction in equational theories with constructors
• On sufficient-completeness and related properties of term rewriting systems
• Parameter-preserving data type specifications
• Termination of rewriting
• Mechanizing structural induction. II: Strategies
• The algebraic specification of abstract data types
• Automated deduction -- CADE-12. 12th international conference, Nancy, France, June 26 -- July 1, 1994. Proceedings
• Linearizing term rewriting systems using test sets
• A strong restriction of the inductive completion procedure
• Automatic proofs by induction in theories without constructors
• Implicit induction in conditional theories
• Abstract data types and software validation
• Automated Mathematical Induction
• Computing ground reducibility and inductively complete positions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item