Ruppert, Eric2018-05-282018-05-282017-12-042018-05-28http://hdl.handle.net/10315/34539We show that correctness criteria of concurrent algorithms are mathematically equivalent to the existence of so-called simulations between implementations of the algorithms in a well-known framework (that of input/output automata) and simple canonical automata. This equivalence allows us to frame our proofs of correctness in a language much more amenable to machine-checking than conventional proofs. We give the first demonstration that when strongly linearizable implementations of randomized concurrent algorithms are utilized, then the distributions of a well-defined class of random variables are preserved under object substitution by non-concurrent implementations of the same algorithms. We also consider weaker conditions than strong linearizability under which implementations are still correct in the presence of randomization.enAuthor owns copyright, except where explicitly noted. Please contact the author directly with licensing requests.Computer scienceElectronic Thesis or Dissertation2018-05-28Computer scienceDistributed computingVerificationRandomized algorithmsSimulationsLinearizabilityStrong linearizability