Proofs in parameterized specifications

DOI10.1007/3-540-53904-2_95MaRDI QIDQ5055758zbMATH OpenOpenAlexFDO

Authors Hélène Kirchner

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-53904-2_95

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 3880082
• scientific article; zbMATH DE number 2079677
• scientific article; zbMATH DE number 1368957
• An automatic proving approach to parameterized verification
• The equational theory of parameterized specifications
• Automated Technology for Verification and Analysis
• Using induction and rewriting to verify and complete parameterized specifications
• Parameterized provability in equational logic
• Publication:3034806
• Proof systems for structured algebraic specifications: An overview

Cites work

• A characterization of passing compatibility for parameterized specifications
• Automatic proofs by induction in theories without constructors
• Computing with rewrite systems
• scientific article; zbMATH DE number 4133477 (Why is no real title available?)
• scientific article; zbMATH DE number 3888893 (Why is no real title available?)
• scientific article; zbMATH DE number 4164137 (Why is no real title available?)
• scientific article; zbMATH DE number 4164142 (Why is no real title available?)
• scientific article; zbMATH DE number 3990847 (Why is no real title available?)
• scientific article; zbMATH DE number 3776841 (Why is no real title available?)
• scientific article; zbMATH DE number 125892 (Why is no real title available?)
• scientific article; zbMATH DE number 4776 (Why is no real title available?)
• On sufficient-completeness and related properties of term rewriting systems
• Parameterized Programming
• Parameterized Specifications: Parameter Passing and Implementation with Respect to Observability
• Semantic confluence tests and completion methods
• Term rewriting induction
• The equational theory of parameterized specifications

Cited in

(13)

• The equational theory of parameterized specifications
• Inductive theorem proving for design specifications
• Specification of parameterized programs -- persistency revisited
• The power of parameterization in coinductive proof
• scientific article; zbMATH DE number 4133477 (Why is no real title available?)
• Proof-Relevant Parametricity
• scientific article; zbMATH DE number 3880082 (Why is no real title available?)
• scientific article; zbMATH DE number 3936501 (Why is no real title available?)
• scientific article; zbMATH DE number 1761886 (Why is no real title available?)
• Proving correctness w.r.t. specifications with hidden parts
• scientific article; zbMATH DE number 6403889 (Why is no real title available?)
• A general framework to build contextual cover set induction provers
• Proving semantical equivalence of data specifications

This page was built for publication: Proofs in parameterized specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055758)