Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32

Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32

In this work, we present an approach towards constructing executable specifications of existing filesystems and verifying their functional properties in a theorem proving environment. We detail an application of this approach to the FAT32 filesystem. We also detail the methodology used to build up...

Full description

Bibliographic Details
Main Author: Mihir Parang Mehta
Format: Article
Language:English
Published: Open Publishing Association 2018-10-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1810.04309v1
id doaj-3b712d0ffb5e41548957e3078c7e2f4e
record_format Article
spelling doaj-3b712d0ffb5e41548957e3078c7e2f4e2020-11-25T02:19:32ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802018-10-01280Proc. ACL2 2018182910.4204/EPTCS.280.2:1Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32Mihir Parang Mehta0 UT Austin In this work, we present an approach towards constructing executable specifications of existing filesystems and verifying their functional properties in a theorem proving environment. We detail an application of this approach to the FAT32 filesystem. We also detail the methodology used to build up this type of executable specification through a series of models which incrementally add features of the target filesystem. This methodology has the benefit of allowing the verification effort to start from simple models which encapsulate features common to many filesystems and which are thus suitable for reuse.http://arxiv.org/pdf/1810.04309v1
collection DOAJ
language English
format Article
sources DOAJ
author Mihir Parang Mehta
spellingShingle Mihir Parang Mehta
Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32
Electronic Proceedings in Theoretical Computer Science
author_facet Mihir Parang Mehta
author_sort Mihir Parang Mehta
title Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32
title_short Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32
title_full Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32
title_fullStr Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32
title_full_unstemmed Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32
title_sort formalising filesystems in the acl2 theorem prover: an application to fat32
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2018-10-01
description In this work, we present an approach towards constructing executable specifications of existing filesystems and verifying their functional properties in a theorem proving environment. We detail an application of this approach to the FAT32 filesystem. We also detail the methodology used to build up this type of executable specification through a series of models which incrementally add features of the target filesystem. This methodology has the benefit of allowing the verification effort to start from simple models which encapsulate features common to many filesystems and which are thus suitable for reuse.
url http://arxiv.org/pdf/1810.04309v1
work_keys_str_mv AT mihirparangmehta formalisingfilesystemsintheacl2theoremproveranapplicationtofat32
_version_ 1724876202798219264

Similar Items