{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T23:59:33Z","timestamp":1791244773964,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540238416","type":"print"},{"value":"9783540304821","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30482-1_32","type":"book-chapter","created":{"date-parts":[[2010,3,1]],"date-time":"2010-03-01T16:27:38Z","timestamp":1267460858000},"page":"373-390","source":"Crossref","is-referenced-by-count":40,"title":["Verifying a File System Implementation"],"prefix":"10.1007","author":[{"given":"Konstantine","family":"Arkoudas","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Karen","family":"Zee","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Kuncak","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"32_CR1","unstructured":"Arkoudas, K.: Athena, www.cag.csail.mit.edu\/~kostas\/dpls\/athena"},{"key":"32_CR2","unstructured":"Arkoudas, K.: Denotational Proof Languages. PhD dissertation, MIT (2000)"},{"key":"32_CR3","doi-asserted-by":"crossref","unstructured":"Arkoudas, K.: Specification, abduction, and proof. In: Second International Symposium on Automated Technology for Verification and Analysis, Taiwan (October 2004)","DOI":"10.1007\/978-3-540-30476-0_25"},{"key":"32_CR4","doi-asserted-by":"crossref","unstructured":"Arkoudas, K., Bringsjord, S.: Metareasoning for multi-agent epistemic logics. In: 5th workshop on Computational Logic in Multi-agent Systems, Lisbon, Portugal (September 2004)","DOI":"10.1007\/11533092_7"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Arkoudas, K., Khurshid, S., Marinov, D., Rinard, M.: Integrating model checking and theorem proving for relational reasoning. In: 7th International Seminar on Relational Methods in Computer Science (2003)","DOI":"10.1007\/978-3-540-24771-5_3"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Arkoudas, K., Rinard, M.: Deductive runtime certification. In: Proceedings of the 2004 Workshop on Runtime Verification, Barcelona, Spain (April 2004)","DOI":"10.1016\/j.entcs.2004.01.035"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Arkoudas, K., Zee, K., Kuncak, V., Rinard, M.: On verifying a file system implementation. Technical Report 946, MIT CSAIL (May 2004)","DOI":"10.1007\/978-3-540-30482-1_32"},{"key":"32_CR8","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Rusinowitch, M., Sehgal, A.K.: High-performance deduction for verification: a case study in the theory of arrays. In: Autexier, S., Mantel, H. (eds.) Notes of the Workshop on Verification, Third Federated Logic Conference (FLoC 2002), pp. 103\u2013112 (2002)"},{"key":"32_CR9","unstructured":"Arvizo, T.: A virtual machine for a type-\u03c9 denotational proof language. Masters thesis, MIT (June 2002)"},{"key":"32_CR10","doi-asserted-by":"crossref","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. ACM PLDI (2001)","DOI":"10.1145\/378795.378846"},{"key":"32_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/10721959_6","volume-title":"Automated Deduction - CADE-17","author":"C.W. Barrett","year":"2000","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: A framework for cooperating decision procedures. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 79\u201398. Springer, Heidelberg (2000)"},{"key":"32_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4edel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)"},{"key":"32_CR13","unstructured":"Brucker, A.D., Rittinger, F., Wolff, B.: A cvs-server security architecture: Concepts and formal analysis. Technical Report 182, Institut f\u00fcr Informatik Albert-Ludwigs-Universit\u00e4t Freiburg, HOL-Z distribution (December 2003), http:\/\/wailoa.informatik.uni-freiburg.de\/holz\/index.html"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Chan, W., Anderson, R.J., Beame, P., Burns, S., Modugno, F., Notkin, D., Reese, J.D.: Model checking large software specifications. IEEE TSE, 498\u2013520 (July 1998)","DOI":"10.1109\/32.708566"},{"key":"32_CR15","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Proc. ACM PLDI (2002)","DOI":"10.1145\/512529.512538"},{"key":"32_CR16","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663079","volume-title":"Data Refinement: Model-oriented proof methods and their comparison","author":"W.-P. Roever de","year":"1998","unstructured":"de Roever, W.-P., Engelhardt, K.: Data Refinement: Model-oriented proof methods and their comparison. Cambridge Tracts in Theoretical Computer Science, vol.\u00a047. Cambridge University Press, Cambridge (1998)"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In: Proc. ACM PLDI (2001)","DOI":"10.1145\/378795.378811"},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"Fradet, P., M\u00e9tayer, D.L.: Shape types. In: Proc. 24th ACM POPL (1997)","DOI":"10.1145\/263699.263706"},{"key":"32_CR19","volume-title":"Introduction to HOL, a theorem proving environment for higher-order logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL, a theorem proving environment for higher-order logic. Cambridge University Press, Cambridge (1993)"},{"key":"32_CR20","unstructured":"Hao, M.: Using a denotational proof language to verify dataflow analyses. Masters thesis, MIT (September 2002)"},{"issue":"2","key":"32_CR21","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM TOSEM\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM TOSEM"},{"key":"32_CR22","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"32_CR23","doi-asserted-by":"crossref","unstructured":"Khurshid, S., Jackson, D.: Exploring the design of an intentional naming scheme with an automatic constraint analyzer. In: 15th IEEE ASE (2000)","DOI":"10.1109\/ASE.2000.873646"},{"key":"32_CR24","doi-asserted-by":"crossref","unstructured":"Klarlund, N., M\u00f8ller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Proc. 5th International Conference on Implementation and Application of Automata. LNCS (2000)","DOI":"10.7146\/brics.v7i40.20206"},{"key":"32_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-540-24622-0_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V. Kuncak","year":"2004","unstructured":"Kuncak, V., Rinard, M.: Boolean algebra of shape analysis constraints. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 59\u201372. Springer, Heidelberg (2004)"},{"key":"32_CR26","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/981009.981016","volume":"39","author":"P. Lam","year":"2004","unstructured":"Lam, P., Kuncak, V., Rinard, M.: Generalized typestate checking using set interfaces and pluggable analyses. SIGPLAN Notices\u00a039, 46\u201355 (2004)","journal-title":"SIGPLAN Notices"},{"key":"32_CR27","doi-asserted-by":"crossref","unstructured":"Larus, J.R., Hilfinger, P.N.: Detecting conflicts between structure accesses. In: Proc. ACM PLDI, Atlanta, GA (June 1988)","DOI":"10.1145\/53990.53993"},{"issue":"3","key":"32_CR28","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/989.990","volume":"2","author":"M.K. McKusick","year":"1984","unstructured":"McKusick, M.K., Joy, W.N., Leffler, S.J., Fabry, R.S.: A fast file system for UNIX. Computer Systems\u00a02(3), 181\u2013197 (1984)","journal-title":"Computer Systems"},{"key":"32_CR29","first-page":"80","volume-title":"Object-oriented Specification Case Studies, ch. 4","author":"S.R.L. Meira","year":"1994","unstructured":"Meira, S.R.L., Cavalcanti, A.L.C., Santos, C.S.: The unix filing system: A MooZ specification. In: Lano, K., Haughton, H. (eds.) Object-oriented Specification Case Studies, ch. 4, pp. 80\u2013109. Prentice-Hall, Englewood Cliffs (1994)"},{"key":"32_CR30","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"32_CR31","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language Reference. SRI International, Computer Science Laboratory, 333 Ravenswood Avenue, Menlo Park CA 94025"},{"key":"32_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1080\/014453499298165","volume":"20","author":"F.J. Pelletier","year":"1999","unstructured":"Pelletier, F.J.: A Brief History of Natural Deduction. History and Philosophy of Logic\u00a020, 1\u201331 (1999)","journal-title":"History and Philosophy of Logic"},{"issue":"3","key":"32_CR33","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1145\/514188.514190","volume":"24","author":"M. Sagiv","year":"2002","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM TOPLAS\u00a024(3), 217\u2013298 (2002)","journal-title":"ACM TOPLAS"},{"key":"32_CR34","doi-asserted-by":"crossref","unstructured":"Thompson, K.: UNIX implementation. The Bell System Technical Journal, 57(6 (part 2)) (1978)","DOI":"10.1002\/j.1538-7305.1978.tb02137.x"},{"issue":"2","key":"32_CR35","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BF00881918","volume":"15","author":"A. Voronkov","year":"1995","unstructured":"Voronkov, A., et al.: The anatomy of Vampire (implementing bottom-up procedures with code trees). JAR\u00a015(2), 237\u2013265 (1995)","journal-title":"JAR"},{"key":"32_CR36","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning, ch. 27","author":"C. Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 27, vol.\u00a0II, pp. 1965\u20132013. Elsevier, Amsterdam (2001)"},{"key":"32_CR37","unstructured":"Wenzel, M.: Isabelle\/Isar \u2014 a versatile environment for human-readable formal proof documents. PhD thesis, Technische Universitaet Muenchen (2002)"},{"key":"32_CR38","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/S0167-6423(96)00020-2","volume":"28","author":"J.M. Wing","year":"1997","unstructured":"Wing, J.M., Vaziri-Farahani, M.: A case study in model checking software systems. Science of Computer Programming\u00a028, 273\u2013299 (1997)","journal-title":"Science of Computer Programming"},{"key":"32_CR39","volume-title":"Using Z","author":"J. Woodcock","year":"1996","unstructured":"Woodcock, J., Davies, J.: Using Z. Prentice-Hall, Inc., Englewood Cliffs (1996)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30482-1_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T17:39:47Z","timestamp":1685468387000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30482-1_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540238416","9783540304821"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30482-1_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}