Flashix: modular verification of a concurrent and crash-safe flash file system

DOI10.1007/978-3-030-76020-5_14MaRDI QIDQ2117600zbMATH OpenOpenAlexFDO

Authors Stefan Bodenmüller, Gerhard Schellhorn, Martin Bitterlich, Wolfgang Reif

Publication date 22 March 2022

Full work available at URL https://opus.bibliothek.uni-augsburg.de/opus4/frontdoor/index/index/docId/87303

Mathematics Subject Classification ID

Mathematical logic and foundations (03-XX) Computer science (68-XX)

Cites work

• scientific article; zbMATH DE number 1615985 (Why is no real title available?)
• scientific article; zbMATH DE number 1650458 (Why is no real title available?)
• scientific article; zbMATH DE number 773979 (Why is no real title available?)
• A calculus of atomic actions
• Abstract State Machines
• Algebraic Methodology and Software Technology
• Completeness of ASM refinement
• Data Refinement
• Modeling in Event B. System and software engineering.
• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Reduction
• Refinement through restraint: bringing down the cost of verification
• The ASM refinement method
• The Rely-Guarantee method for verifying shared variable concurrent programs
• The WAM case study: Verifying compiler correctness for Prolog with KIV
• Verifying correctness of persistent concurrent data structures: a sound and complete method

Describes a project that uses

Uses Software

• RGITL
• Rodin

This page was built for publication: Flashix: modular verification of a concurrent and crash-safe flash file system

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