Using model checking to find serious file system errors

By Junfeng Yang, Paul Twohey, Dawson R. Engler, M. Musuvathi. TOCS, 2004

379 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Overcoming an Untrusted Computing Base: Detecting and Removing Malicious Hardware Automatically (2010, methodology): “Formal methods such as symbolic execution [9, 10], model checking [6, 13, 28], and information flow [23, 29] have been applied to software systems for better test coverage and improved security analysis.”
Finding and Reproducing Heisenbugs in Concurrent Programs (2008, positive): “Second, C HESS uses systematic enumeration techniques [10, 37, 17, 31, 45, 22] to force every run of the program along a different thread interleaving.”
Zyzzyva (2007, background): “non-fail-stop behavior in real systems [2, 5, 6, 27, 30, 32, 36, 39, 40] suggest that BFT may yield significant benefits even without resorting to n-version programming [4, 15, 33].”
Software model checking (2009, positive): “CMC has been used to ﬁnd errors in implementations of network protocols [Musuvathi and Engler 2004] and ﬁle systems [Yang et al. 2004].”
Improving the reliability of commodity operating systems (2005, methodology): “However, model checking can find bugs (but not prove correctness) by checking a much smaller number of states [211].”
Using Crash Hoare logic for certifying the FSCQ file system (2015, background): “Model-checking [67–69] and fuzz-testing [35] techniques are e ff ective at detecting file-system bugs.”