Spelling suggestions: "subject:"file atemsystem VCC formal aerification"" "subject:"file atemsystem VCC formal erification""
1 |
Analýza souborového systému pomocí Verifying C Compiler / Analysis of a File System Using the Verifying C CompilerŠkorvaga, David January 2015 (has links)
Title: Analysis of a File System Using the Verifying C Compiler Author: Bc. David Škorvaga Department: Department of Distributed and Dependable Systems Supervisor: RNDr. Jan Kofroň, Ph.D. Abstract: Formal verification is a way to improve reliability of software systems. One approach of formal verification is focused on proving correctness of annotat- ed source code of an established programming language. Verifying C Compiler (VCC) is a verifier for concurrent C that accepts an annotated code in C language and automatically verifies its correctness with respect to the given annotation. There have been successful attempts to verify some critical systems, including the operating system kernel. Another critical part of operating system is its file system. In the thesis, we choose FatFs file system, a simple device-independent implementation of the FAT file system. We specify a part of it using the VCC annotation and successfully verify its correctness. Keywords: Formal Verification, File System, VCC
|
Page generated in 0.1313 seconds