Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Discipline
Articles 1 - 2 of 2
Full-Text Articles in Physical Sciences and Mathematics
A Machine-Verified Proof Of Linearizability For A Queue Algorithm, Ugur Yavuz
A Machine-Verified Proof Of Linearizability For A Queue Algorithm, Ugur Yavuz
Dartmouth College Master’s Theses
Proofs of linearizability are typically intricate and lengthy, and readers may find it difficult to verify their correctness. We present a unique technique for producing proofs of linearizability that are fully verifiable by a mechanical proof system, thereby eliminating the need for any manual verification. Specifically, we reduce the burden of proving linearizable object implementations correct to the proof of a particular invariant whose correctness can be shown inductively. Noting that the latter is a task that many proof systems (such as the TLA+ Proof System we chose to work with) are well-suited to handle, this technique allows us to …
Producing Easy-To-Verify Proofs Of Linearizability, Ugur Yavuz
Producing Easy-To-Verify Proofs Of Linearizability, Ugur Yavuz
Computer Science Senior Theses
Proofs of linearizability tend to be complex and lengthy, rendering their verification challenging for readers. We provide a novel technique to produce easy-to-verify proofs of linearizability, with the help of mechanical proof assistants. Specifically, we reduce the task of proving the correctness of a linearizable object implementation, to a proof of an inductive invariant of a slightly modified version of the implementation. As the latter is a task many mechanical proof systems (such as TLAPS) are well-suited to undertake, this reduction allows the verification of the proof by the reader, to only consist of a trivial syntactic check of whether …