Modular correctness proofs of behavioural implementations

DOI10.1007/S002360050149MaRDI QIDQ1127821zbMATH OpenOpenAlexFDO

Authors Rolf Hennicker, Michel Bidoit

Publication date 29 March 1999

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s002360050149

zbMATH Keywords

algebraic specificationsbehavioural equality

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Recommendations

• Proving the correctness of behavioural implementations
• Modular Verification of Recursive Programs
• On the correctness of modular systems
• Modular verification of higher-order functional programs
• Modular verification of programs with effects and effects handlers
• Correctness proofs for abstract implementations
• Formal reasoning about modules, reuse and their correctness

Cited in

(12)

• scientific article; zbMATH DE number 1696758 (Why is no real title available?)
• Observational implementation of algebraic specifications
• A semi-algorithm for algebraic implementation proofs
• On the correctness of modular systems
• Proving Behavioral Refinements of COL-specifications
• On behavioural abstraction and behavioural satisfaction in higher-order logic
• Proving the correctness of behavioural implementations
• scientific article; zbMATH DE number 17803 (Why is no real title available?)
• Observational interpretation of Casl specifications
• Behavioral abstraction is hiding information
• Towards behavioral Maude: behavioral membership equational logic
• scientific article; zbMATH DE number 3921953 (Why is no real title available?)

Describes a project that uses

Uses Software

• LARCH

This page was built for publication: Modular correctness proofs of behavioural implementations

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