Name: Jiri Simsa 

 Place: Carnegie Mellon University
 Status: PhD student
 Area: Formal methods
 Advisors: Randy Bryant and Garth Gibson

File Systems Readings

  • Howard, J. H., Kazar, M. L., Menees, S. G., Nichols, D. A., Satyanarayanan, M., Sidebotham, R. N., and West, M. J. 1988. Scale and performance in a distributed file system. ACM Trans. Comput. Syst. 6, 1 (Feb. 1988), 51-81.
  • Patterson, D. A., Gibson, G., and Katz, R. H. 1988. A case for redundant arrays of inexpensive disks (RAID). In Proceedings of the 1988 ACM SIGMOD international Conference on Management of Data (Chicago, Illinois, United States, June 01 - 03, 1988). H. Boral and P. Larson, Eds. SIGMOD '88. ACM Press, New York, NY, 109-116.
  • Rosenblum, M. and Ousterhout, J. K. 1992. The design and implementation of a log-structured file system. ACM Trans. Comput. Syst. 10, 1 (Feb. 1992), 26-52.
  • Amiri, K., Gibson, G. A., and Golding, R. 2000. Highly Concurrent Shared Storage. In Proceedings of the the 20th international Conference on Distributed Computing Systems ( ICDCS 2000) (April 10 - 13, 2000). ICDCS. IEEE Computer Society, Washington, DC, 298.
  • Adya, A., Bolosky, W. J., Castro, M., Cermak, G., Chaiken, R., Douceur, J. R., Howell, J., Lorch, J. R., Theimer, M., and Wattenhofer, R. P. 2002. Farsite: federated, available, and reliable storage for an incompletely trusted environment. SIGOPS Oper. Syst. Rev. 36, SI (Dec. 2002), 1-14.
  • A. Birrell, A. Hisgen, C. Jerian, T. Mann, and G. Swart. The Echo Distributed File System. DEC SRC Technical Report 111. October 1993.
  • Gibson, G. A., Nagle, D. F., Amiri, K., Butler, J., Chang, F. W., Gobioff, H., Hardin, C., Riedel, E., Rochberg, D., and Zelenka, J. 1998. A cost-effective, high-bandwidth storage architecture. In Proceedings of the Eighth international Conference on Architectural Support For Programming Languages and Operating Systems (San Jose, California, United States, October 02 - 07, 1998). ASPLOS-VIII. ACM Press, New York, NY, 92-103.
  • Ghemawat, S., Gobioff, H., and Leung, S. 2003. The Google file system. SIGOPS Oper. Syst. Rev. 37, 5 (Dec. 2003), 29-43.
  • McKusick, M. K. and Neville-Neil, G. V. 2004 The Design and Implementation of the FreeBSD Operating System. Pearson Education.
  • Bolosky, W. J., Douceur, J. R., and Howell, J. 2007. The Farsite project: a retrospective. SIGOPS Oper. Syst. Rev. 41, 2 (Apr. 2007), 17-26.
  • Schroeder, B. and Gibson, G. A. 2007. Disk failures in the real world: what does an MTTF of 1,000,000 hours mean to you?. In Proceedings of the 5th Conference on USENIX Conference on File and Storage Technologies - Volume 5 (San Jose, CA, February 13 - 16, 2007). USENIX Association, Berkeley, CA, 1-16.

Formal Verification Readings:

  • Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2003. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50, 5 (Sep. 2003), 752-794.

File Systems Formal Verification Readings:

  • Groce, A., Holzmann, G., and Joshi, R. 2006. New Challenges in Model Checking. In Symposium on 25 Years of Model Checking, Seattle, Washington, August 2006.
  • Groce, A., Holzmann, G., and Joshi, R. 2007. Randomized Differential Testing as a Prelude to Formal Verification. In Proceedings of the 29th international Conference on Software Engineering (May 20 - 26, 2007). International Conference on Software Engineering. IEEE Computer Society, Washington, DC, 621-631.
Home