CMU-CS-19-100Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-19-100
Joseph Tassarotti Ph.D. Thesis January 2019
Keywords:
Concurrency, program logics, separation logic, randomized algorithms, verification
Concurrency and randomization are diffiult to use correctly when programming. Because programs that use them no longer behave deterministically, programmers must take into account the set of all possible interactions and random choices that may occur. This dissertation describes a logic for reasoning about programs using both of these effects. The logic extends a recent concurrent separation logic with ideas from denotational semantics for probabilistic and nondeterministic choice, along with principles for probabilistic relational reasoning originally developed for sequential programs. The resulting logic is used to verify probabilistic behaviors of a randomized concurrent counter algorithm and a twolevel concurrent skip list. The soundness of the logic, as well as the proofs of these examples, have been mechanized in Coq. 134 pages
Srinivasan Seshan, Head, Computer Science Department
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |