Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
Articles 1 - 2 of 2
Full-Text Articles in Physical Sciences and Mathematics
Space-Efficient Algorithms And Verification Schemes For Graph Streams, Prantar Ghosh
Space-Efficient Algorithms And Verification Schemes For Graph Streams, Prantar Ghosh
Dartmouth College Ph.D Dissertations
Structured data-sets are often easy to represent using graphs. The prevalence of massive data-sets in the modern world gives rise to big graphs such as web graphs, social networks, biological networks, and citation graphs. Most of these graphs keep growing continuously and pose two major challenges in their processing: (a) it is infeasible to store them entirely in the memory of a regular server, and (b) even if stored entirely, it is incredibly inefficient to reread the whole graph every time a new query appears. Thus, a natural approach for efficiently processing and analyzing such graphs is reading them as …
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 …