GoTxn: Verifying a Crash-Safe, Concurrent Transaction System

Bugs related to concurrency and crash safety are infamous for being subtle and hard to reproduce. Formal verification provides a way to combat such bugs through the use of machine-checked proofs about program behavior. However, reasoning about concurrency and crashes can be tricky, especially when s...

Full description

Bibliographic Details
Main Author: Theng, Mark
Other Authors: Kaashoek, M. Frans
Format: Thesis
Published: Massachusetts Institute of Technology 2022
Online Access:https://hdl.handle.net/1721.1/143253