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

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

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)

Cites Work

• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Abstract State Machines
• Title not available (Why is that?)
• Title not available (Why is that?)
• The ASM refinement method
• Title not available (Why is that?)
• The Rely-Guarantee method for verifying shared variable concurrent programs
• Completeness of ASM Refinement
• The WAM case study: Verifying compiler correctness for Prolog with KIV
• Reduction
• Title not available (Why is that?)
• Algebraic Methodology and Software Technology
• Data Refinement
• A calculus of atomic actions
• Verifying correctness of persistent concurrent data structures: a sound and complete method
• Refinement through restraint: bringing down the cost of verification

Uses Software

• Rodin
• RGITL

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)