DROPS

Found 2 Possible Name Variants:

Cook, William R.
Cook, William

Cook, William R.

Document

DOI: 10.4230/LIPIcs.ITP.2019.25

Binary-Compatible Verification of Filesystems with ACL2

Authors: Mihir Parang Mehta and William R. Cook

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract

Filesystems are an essential component of most computer systems. Work on the verification of filesystem functionality has been focused on constructing new filesystems in a manner which simplifies the process of verifying them against specifications. This leaves open the question of whether filesystems already in use are correct at the binary level. This paper introduces LoFAT, a model of the FAT32 filesystem which efficiently implements a subset of the POSIX filesystem operations, and HiFAT, a more abstract model of FAT32 which is simpler to reason about. LoFAT is proved to be correct in terms of refinement of HiFAT, and made executable by enabling the state of the model to be written to and read from FAT32 disk images. EqFAT, an equivalence relation for disk images, considers whether two disk images contain the same directory tree modulo reordering of files and implementation-level details regarding cluster allocation. A suite of co-simulation tests uses EqFAT to compare the operation of existing FAT32 implementations to LoFAT and check the correctness of existing implementations of FAT32 such as the mtools suite of programs and the Linux FAT32 implementation. All models and proofs are formalized and mechanically verified in ACL2.

Cite as

Mihir Parang Mehta and William R. Cook. Binary-Compatible Verification of Filesystems with ACL2. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{mehta_et_al:LIPIcs.ITP.2019.25,
  author =	{Mehta, Mihir Parang and Cook, William R.},
  title =	{{Binary-Compatible Verification of Filesystems with ACL2}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{25:1--25:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.25},
  URN =		{urn:nbn:de:0030-drops-110807},
  doi =		{10.4230/LIPIcs.ITP.2019.25},
  annote =	{Keywords: interactive theorem proving, filesystems}
}

Cook, William

Document

DOI: 10.4230/DagRep.1.1.27

Feature-Oriented Software Development (FOSD) (Dagstuhl Seminar 11021)

Authors: Sven Apel, William Cook, Krzysztof Czarnecki, and Oscar Nierstrasz

Published in: Dagstuhl Reports, Volume 1, Issue 1 (2011)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 11021 "Feature-Oriented Software Development (FOSD)". FOSD is an emerging paradigm that aims at increasing the level of automation, reuse, and variation in software development. The main goal of the Dagstuhl seminar on FOSD was to gather researchers and practitioners who are active in different communities to discuss the roots, state of the art, and future directions of FOSD research and practice. Additional goals were to strengthen the identity of the feature orientation community and to relate FOSD to other software development paradigms. The report contains an executive summary, abstracts of the talks held during the seminar, and summaries of special sessions.

Cite as

Sven Apel, William Cook, Krzysztof Czarnecki, and Oscar Nierstrasz. Feature-Oriented Software Development (FOSD) (Dagstuhl Seminar 11021). In Dagstuhl Reports, Volume 1, Issue 1, pp. 27-41, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@Article{apel_et_al:DagRep.1.1.27,
  author =	{Apel, Sven and Cook, William and Czarnecki, Krzysztof and Nierstrasz, Oscar},
  title =	{{Feature-Oriented Software Development (FOSD) (Dagstuhl Seminar 11021)}},
  pages =	{27--41},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2011},
  volume =	{1},
  number =	{1},
  editor =	{Apel, Sven and Cook, William and Czarnecki, Krzysztof and Nierstrasz, Oscar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.1.1.27},
  URN =		{urn:nbn:de:0030-drops-31414},
  doi =		{10.4230/DagRep.1.1.27},
  annote =	{Keywords: FOSD, automation, software family}
}

Search Results

Documents authored by Cook, William R.

Cook, William R.

Binary-Compatible Verification of Filesystems with ACL2

Abstract

Cite as

Cook, William

Feature-Oriented Software Development (FOSD) (Dagstuhl Seminar 11021)

Abstract

Cite as

Thanks for your feedback!

Could not send message