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

DOI10.1007/978-3-030-76020-5_14OpenAlexW3166142592MaRDI QIDQ2117600

Martin Bitterlich, Gerhard Schellhorn, Stefan Bodenmüller, 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)

Uses Software

• Rodin
• RGITL

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The ASM refinement method
• The Rely-Guarantee method for verifying shared variable concurrent programs
• Verifying correctness of persistent concurrent data structures: a sound and complete method
• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Refinement through restraint: bringing down the cost of verification
• Reduction
• Abstract State Machines
• A calculus of atomic actions
• Data Refinement
• Algebraic Methodology and Software Technology
• Completeness of ASM Refinement