FAQ

• What exactly is it that the model models? (What is the "essence" of a file system?)

• What sorts of interleaving/concurrency does the model handle? What about two racing writes, can they interleave?

• How is the equivalence partitioning and trace generation implemented?

• Is it surprising that more bugs weren't found, particularly security bugs?

• Why don't you test for concurrent/racy file system bugs?

• How was the model constructed?