Overview on methods for model checking:
- Model Checking: Algorithmic Verification and Debugging
- Linear Temporal Logic Symbolic Model Checking
Model Checking in Distributed Storage Systems:
- Rabia: Simplifying State-Machine Replication Through Randomization (SOSP'21)
- Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3 (SOSP'21)
- SAMC: Semantic-Aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems (OSDI'14)
- MODIST: Transparent Model Checking of Unmodified Distributed Systems (NSDI'09)
Model Checking in Local Storage Systems:
- Model-Checking Support for File System Development (HotStorage'21)
- Jaaru: Efficiently Model Checking Persistent Memory Programs (ASPLOS'21)
- Storage Systems are Distributed Systems (So Verify Them That Way!) (OSDI'20)
- Push-Button Verification of File Systems via Crash Refinement (OSDI'16)
- Specifying and Checking File System Crash-Consistency Models (ASPLOS'16)
- SibylFS: formal specification and oracle-based testing for POSIX and real-world file systems (SOSP'15)
- EXPLODE: A Lightweight, General Approach to Finding Serious Errors in Storage Systems (OSDI'06)