Concurrency and randomization are two programming features that are notoriously difficult to use correctly. This is because programs that use them no longer behave deterministically, so programmers must take into account the set of all possible interactions and random choices that may occur. A common approach to reasoning about complex programs is to use relational or refinement reasoning: to understand a complex program, we first prove a correspondence between its behavior and that of some simpler program. Then, we can analyze or verify properties of this simpler program and draw conclusions about the original program.
Although logics have been developed for relational reasoning for concurrent programs and randomized programs, no logics exist for reasoning about programs that are both concurrent and randomized. I propose developing a program logic that supports reasoning about both of these features. Moreover, I argue that such a logic is more than just an ad-hoc combination of features: instead, the ideas of separation and resources, which are already central to modern concurrency logics, also provide a foundation for probabilistic reasoning.
Thesis Committee: Robert Harper (Chair) Jan Hoffmann Jeremy Avigad Derek Dreyer (MPI-SWS)