Cogent: Verifying High-Assurance File System Implementations

Alex Hixon
Alex Hixon
Peter Chubb
Peter Chubb
Liam O'Connor
Liam O'Connor
Joel Beeren
Joel Beeren
Yutaka Nagashima
Yutaka Nagashima
Joseph Tuong
Joseph Tuong

Special Interest Group on Programming Languages, pp. 175-188, 2016.

Cited by: 69|Views58
EI

Abstract:

We present an approach to writing and formally verifying high-assurance file-system code in a restricted language called Cogent, supported by a certifying compiler that produces C code, high-level specification of Cogent, and translation correctness proofs. The language is strongly typed and guarantees absence of a number of common file s...More

Code:

Data:

Get fulltext within 24h
Bibtex
Upload PDF

1.Your uploaded documents will be check within 24h, and coins will be credited to your account.

2.As the current system does not support cash withdrawal, you can add staff WeChat (AMxiaomai) to receive it as a red packet.

3.10 coins will be exchanged for 1 yuan.

?

Upload a single paper

for 5 coins

Wechat's Red Packet
?

Upload 50 articles

for 280 coins

Wechat's Red Packet
?

Upload 200 articles

for 1200 coins

Wechat's Red Packet
?

Upload 500 articles

for 3000 coins

Wechat's Red Packet
?

Upload 1000 articles

for 7000 coins

Wechat's Red Packet
Your rating :
0

 

Tags
Comments