Recent progress in systems verification have shown that verification techniques
can scale to thousands of lines. It is time to ask whether verification can
displace testing as an effective path to software correctness.
The veribetrfs project is developing a verified high-performance storage
system. A primary goal of the project is to reduce verification methodology to
engineering practice. Veribetrfs is developed using the Iron★ methodology, a
descendent of the Ironclad and IronFleet projects. So far, we have a key-value
store with 100k iops performance and strong guarantees against data loss. …
Recent progress in systems verification have shown that verification techniques
can scale to thousands of lines. It is time to ask whether verification can
displace testing as an effective path to software correctness.
The veribetrfs project is developing a verified high-performance storage
system. A primary goal of the project is to reduce verification methodology to
engineering practice. Veribetrfs is developed using the Iron★ methodology, a
descendent of the Ironclad and IronFleet projects. So far, we have a key-value
store with 100k iops performance and strong guarantees against data loss. This
talk will give an overview of the methodology and describe how we have enhanced
it in veribetrfs.Â
Read more