Verifying a File System Implementation
Lecture notes in computer sciencePublished 1 January 2004
Konstantine Arkoudas, Karen Zee, Viktor Kunčak, Martin Rinard
Citations67
SJR quartileQ2
SJR score0.35
SNIP0.55
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
This work proves the implementation of a basic file system implementation correct by establishing a simulation relation between the specification of the file system and its implementation (which uses fixed-size disk blocks to store the contents of the files).
Abstract
We present a correctness proof for a basic file system implementation. This implementation contains key elements of standard Unix file systems such as inodes and fixed-size disk blocks. We prove the implementation correct by establishing a simulation relation between the specification of the file system (which models the file system as an abstract map from file names to sequences of bytes) and its implementation (which uses fixed-size disk blocks to store the contents of the files). We used the Athena proof system to represent and validate our proof. Our experience indicates that Athena's use of block-structured natural deduction, support for structural induction and proof abstraction, and seamless integration with high-performance automated theorem provers were essential to our ability to successfully manage a proof of this size.
Keywords
Computer Science
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
2,309 Citations2002Tobias Nipkow, Markus Wenzel +1 more
This presentation discusses Functional Programming in HOL, which aims to provide students with a clear understanding of functional programming and its applications in the real world.
Lecture notes in computer scienceIsabelle/HOL
1,501 Citations2002
This isabelle hol a proof assistant for higher order logic, it will really give you the good idea to be successful.
Cambridge University Press eBooksIntroduction to HOL: a theorem proving environment for higher order logic
1,308 Citations1993Mike Gordon, Tom Melham
A tutorial on goal-directed proof: tactics and tacticals and theorem-Proving With HOL, a simple proof tool for goal-oriented proof of the binomial theorem.
ACM Transactions on Software Engineering and MethodologyAlloy
1,170 Citations2002Daniel Jackson
This paper presents the Alloy language in its entirety, and explains its motivation, contributions and deficiencies.
Lecture notes in computer scienceAnalysis of Recursive Game Graphs Using Data Flow Equations
1,129 Citations2004Kousha Etessami
Given a finite-state abstraction of a sequential program with potentially recursive procedures and input from the environment, whether there are input sequences that can drive the system into “bad/good” executions is checked.
ACM Transactions on Programming Languages and SystemsParametric shape analysis via 3-valued logic
784 Citations2002Mooly Sagiv, Thomas Reps +1 more
A parametric framework for shape analysis that can be instantiated in different ways to create different shape-analysis algorithms that provide varying degrees of efficiency and precision is presented.
ACM Transactions on Computer SystemsA fast file system for UNIX
745 Citations1984Marshall Kirk McKusick, William N. Joy +2 more
A reimplementation of the UNIX TM file system is described, which provides substantially higher throughput rates by using more flexible allocation policies that allow better locality of reference and can be adapted to a wide range of peripheral and processor characteristics.
ACM SIGPLAN NoticesAutomatic predicate abstraction of C programs
703 Citations2012Thomas Ball, Rupak Majumdar +2 more
This work presents the first algorithm to automatically construct a predicate abstraction of programs written in am industrial programming language such as C, and its implementation in a tool -- C2BP, part of the SLAM toolkit.
ESP
544 Citations2002Manuvir Das, Sorin Lerner +1 more
This paper presents a new algorithm for partial program verification that runs in polynomial time and space, and shows that property simulation scales to large programs and is accurate enough to verify meaningful properties.
Enforcing high-level protocols in low-level software
487 Citations2001Robert DeLine, Manuel Fähndrich
The utility of this approach is validated by enforcing protocols present in the interface between the Windows 2000 kernel and its device drivers, which enforces statically that resources cannot be leaked.
Automatic predicate abstraction of C programs
432 Citations2001Thomas Ball, Rupak Majumdar +2 more
This work presents the first algorithm to automatically construct a predicate abstraction of programs written in an industrial programming language such as C, and its implementation in a tool — C2BP.
Information and ComputationForward and Backward Simulations
402 Citations1995Nancy Lynch, Frits Vaandrager
A unified, comprehensive presentation of simulation techniques for verification of concurrent systems is given, in terms of a simple untimed automaton model, where history and prophecy relations are defined and it is shown how invariants can be incorporated into all the simulations.
Flow-sensitive type qualifiers
377 Citations2002Jeffrey S. Foster, Tachio Terauchi +1 more
An efficient constraint-based inference algorithm is obtained that integrates flow-insensitive alias analysis, effect inference, and ideas from linear type systems to support strong updates.
Medical Entomology and ZoologyData Refinement: Model-Oriented Proof Methods and their Comparison
318 Citations2008W.P. deRoever, Kai Engelhardt
The authors concentrate in the first part on the general principles needed to prove data refinement correct, and begin with an explanation of the fundamental notions, showing that data refinement proofs reduce to proving simulation.
Model checking large software specifications
309 Citations1996Richard Anderson, Paul Beame +5 more
The results and experiences of using symbolic model checking to study the specification of an aircraft collision avoidance system and the approach to translating the specification to the SMV language and methods for achieving acceptable performance are reported.
ACM SIGPLAN NoticesDetecting conflicts between structure accesses
214 Citations1988James R. Larus, Paul Hilfinger
Cambridge University Press eBooksData Refinement
205 Citations1998Willem-Paul de Roever, Kai Engelhardt
IEEE Transactions on Software EngineeringModel checking large software specifications
197 Citations1998W. K. Chan, Richard Anderson +5 more
Computer-aided reasoning : ACL2 case studies
178 Citations2000Matt Kaufmann, Panagiotis Manolios +1 more
This chapter defines a function that finds a path between two given nodes of a given directed graph, if such a path exists, and proves the function terminates and it is proved that it is correct.
Lecture notes in computer scienceSymbolic Implementation of the Best Transformer
155 Citations2004Thomas Reps, Mooly Sagiv +1 more
This paper shows how to achieve, under certain conditions, abstract-interpretation algorithms that enjoy the best possible precision for a given abstraction.
Detecting conflicts between structure accesses
153 Citations1988James R. Larus, Paul Hilfinger
This paper describes a dataflow computation that produces a conservative description of the aliases visible at any point in a program that shows how alias graphs can be used to detect potential conflicts.
Lecture notes in computer scienceAutomated Deduction - CADE-17
144 Citations2000David McAllester, MacAllester, David
International Journal of Foundations of Computer ScienceMONA IMPLEMENTATION SECRETS
136 Citations2002Nils Klarlund, Anders Møller +1 more
A selection of implementation "secrets" that have been discovered and tested over the years, including formula reductions, DAGification, guided tree automata, three-valued logic, eager minimization, BDD-based automata representations, and cache-conscious data structures are presented.
mediaTUM – the media and publications repository of the Technical University Munich (Technical University Munich)Isabelle/Isar --- a versatile environment for human-readable formal proof documents
135 Citations2002Markus Wenzel
This work aims to make formal theory developments with machine-checked proofs accessible to a broader audience, and demonstrates that the Isar concepts are indeed sufficiently versatile to cover a broad range of applications.
Bell System Technical JournalUNIX Time-Sharing System: UNIX Implementation
127 Citations1978K. Thompson
This paper describes in high-level terms the implementation of the resident uNIX∗ kernel and describes how the UNIX system views processes, users, and programs.
Shape types
99 Citations1997Pascal Fradet, Daniel Le Métayer
This work provides a syntax for a smooth integration of shape types defined as context-free graph grammars, and defines graphs in set-theoretic terms, and graph modifications as multiset rewrite rules.
UNIX implementation
95 Citations1986K.D. Thompson
This paper describes in high-level terms the implementation of the resident UNIX† kernel and describes how the UNIX system views processes, users, and programs.
Journal of Automated ReasoningThe anatomy of vampire
85 Citations1995Андрей Воронков
The abstract subsumption machine makes subsumption-check using sequences of instructions that are similar to the WAM instructions, which gives an efficient implementation of the “clause at a time” subsumption problem.
History and Philosophy of LogicA Brief History of Natural Deduction
74 Citations1999Francis Jeffry Pelletier
Lecture notes in computer scienceVerifying a File System Implementation
67 Citations2004Konstantine Arkoudas, Karen Zee +2 more
This work proves the implementation of a basic file system implementation correct by establishing a simulation relation between the specification of the file system and its implementation (which uses fixed-size disk blocks to store the contents of the files).
Exploring the design of an intentional naming scheme with an automatic constraint analyzer
48 Citations2000Sarfraz Khurshid, Daniel Jackson
This work constructed a model of INS in Alloy a lightweight relational notation, and analyzed it with the Alloy Constraint Analyzer, a fully automatic simulation and checking tool, exposing several serious flaws in both the algorithm of INS and the underlying naming semantics.
DSpace@MIT (Massachusetts Institute of Technology)Denotational proof languages
46 Citations2000Konstantinos Arkoudas, Olin Shivers
The theory of CND is developed in detail, its soundness and completeness are proved, dozens of sample proofs are presented, and the λμ-calculus is introduced, a terse formal system that can be viewed as a unifying framework for DPLs.
Lecture notes in computer scienceIntegrating Model Checking and Theorem Proving for Relational Reasoning
42 Citations2004Konstantine Arkoudas, Sarfraz Khurshid +2 more
Prioni is a tool that integrates model checking and theorem proving for relational reasoning and uses Athena, a denotational proof language for proof discovery and checking.
Science of Computer ProgrammingA case study in model checking software systems
42 Citations1997Jeannette M. Wing, Mandana Vaziri-Farahani
This work verified three cache coherence protocols used in distributed file systems by using McMillan's SMV model checker and found that on the most complicated protocol, SMV took less than 1 s to check over 43600 reachable states.
ACM SIGPLAN NoticesGeneralized typestate checking using set interfaces and pluggable analyses
35 Citations2004Patrick Lam, Viktor Kunčak +1 more
A generalization of standard typestate systems in which the typestate of each object is determined by its membership in a collection of abstract typestate sets, which characterizes global sharing patterns.
Lecture notes in computer scienceA Framework for Cooperating Decision Procedures
26 Citations2000Clark Barrett, David L. Dill +1 more
A flexible framework for cooperating decision procedures is presented and the properties needed to ensure correctness are described and applied to implement an efficient version of Nelson and Oppen's algorithm for combining decision procedures.
ACM SIGACT NewsReview of "The classical decision problem" by Egon Börger,Erich Grädel and Yuri Gurevich. Springer-Verlag 1997.
22 Citations2004Dan A. Simovici
This book is dedicated to a comprehensive presentation of the classical decision problem of firstorder logic and the notion of reduction class that is a mainstay of the treatment of decidability is also introduced in this initial chapter.
Electronic Notes in Theoretical Computer ScienceDeductive Runtime Certification
19 Citations2005Konstantine Arkoudas, Martin Rinard
A notion of certified computation whereby an algorithm not only produces a result r for a given input x, but also proves that r is a correct result for x, which can greatly enhance the credibility of the result.
Lecture notes in computer scienceMetareasoning for Multi-agent Epistemic Logics
17 Citations2005Konstantine Arkoudas, Selmer Bringsjord
An encoding of a sequent calculus for a multiagent epistemic logic in Athena, an interactive theorem proving system for many-sorted first-order logic is presented and a tactic for solving the generalized version of the wise men problem is developed.
Lecture notes in computer scienceBoolean Algebra of Shape Analysis Constraints
15 Citations2004Viktor Kunčak, Martin Rinard
A family of formulas in (classical, two-valued) logic that are isomorphic to three-valued structures and represent the same sets of concrete states are introduced.
DSpace@MIT (Massachusetts Institute of Technology)A Virtual Machine for a Type-omega Denotational Proof Language
13 Citations2002Teodoro Arvizo
This thesis includes details on the design and implementation of a readeval-print loop that glues together the VM core and the compiler to provide a full, user-accessible interface to monomorphic Athena.
Lecture notes in computer scienceSpecification, Abduction, and Proof
8 Citations2004Konstantine Arkoudas
A case study of railroad safety is used to illustrate several aspects of Athena, a new interactive proof system that supports specification, structured natural deduction proofs, and trusted tactics, and places heavy emphasis on automation.
High-performance deduction for verification: a case study in the theory of arrays
7 Citations2002Alessandro Armando, Maria Paola Bonacina +2 more
An approach to use ordering-based theorem-proving strategies as satisfiability procedures for certain decidable theories, showing that a theorem prover – the E system – compares favorably with the state-of-the-art validity checker CVC.
White Rose Research Online (University of Leeds, The University of Sheffield, University of York)A CVS-Server Security Architecture — Concepts and Formal Analysis
5 Citations2002Achim D. Brucker, Frank Rittinger +1 more
The CVS-server is uses cvsauth, that provides protection of passwords and protection of some internal data of the CVS repository and the approach can be seen as a method to give a formal underpinning for the usually tricky business of system administrators.
DSpace@MIT (Massachusetts Institute of Technology)Using a denotational proof language to verify dataflow analyses
3 Citations2002Melissa B. Hao
A forage harvester of the type having a rotary reel cutterhead and a feedRoll mechanism for feeding crops to the cutterhead is provided with improved drive means for the feed roll mechanism.