Deductive reasoning about concurrent probabilistic programs

In this dissertation, we consider concurrent programs, probabilistic programs and especially the combination of both. To reason about concurrent programs, we facilitate (classical) separation logic to derive axiomatic semantics. Separation logic allows us to declare a separation of heaps. That is, we can declare that predicates hold at different locations in the heap. We can thus partition the heap into a sub-heap used by each thread and a sub-heap used by multiple threads: the shared memory. This idea constitutes concurrent separation logic. For probabilistic programs, we use quantitative logics, which allow us to define a mapping from a random variable and an initial state to the expected value of the respective random variable after executing the given probabilistic program with the given initial state. A quantitative logic differs from a classical logic in that it does not map models to Boolean values, but to real values. Our used quantitative logics also allow for separation operations and thus constitute quantitative separation logics. Using this quantitative logic, we can derive axiomatic semantics to prove an upper bound on the expected value of a random variable. To finally reason about concurrent and probabilistic programs, we combine the techniques to reason about concurrent programs and to reason about probabilistic programs. We thus introduce a fuzzy separation logic for concurrent and probabilistic programs by combining the method to deal with shared memory in concurrent separation logic and the method to deal with expected values in quantitative separation logic. A fuzzy logic maps models to real values between zero and one. This enables us to derive axiomatic semantics to reason about lower bounds of the probability that the program terminates in a certain set of states or does not terminate. The usage of the presented axiomatic semantics requires entailments in the respective logic to be proven. A quantitative or fuzzy entailment is the point-wise lifting of the less-than-or-equals relation. This constitutes a challenge as entailments in the logic without restrictions are undecidable. We thus consider one technique to reason about entailments in fuzzy separation logic and one technique to reason about entailments in quantitative separation logic with user-defined predicates. To reason about entailments in fuzzy separation logic, we transform the entailment into an entailment in classical separation logic. This allows the use of a rich landscape of tools designed for entailments in classical separation logic. We present a restricted syntax which allows the fuzzy part to be solved automatically, while discharging the separation logic part to separation logic entailment checkers. This restricted syntax allows formulae whose semantics has finite image. The second technique allows proving entailments in quantitative separation logic with quantitative user-defined predicates. Quantitative user-defined predicates are given using recursive specifications. With these, we can define predicates that describe the shape for data structures or measure their size. To reason about recursively-defined predicates, we use cyclic proofs. A cyclic proof allows back-linking in proofs to reuse previous proof statements. Such a proof is unsound in general. We introduce a progress criterion on these proofs to guarantee soundness. It turns out that the classic progress criterion using unfoldings of predicates on the left-hand side of the entailment is not easily applicable to quantitative logics. Instead we use heap sizes as our progress criterion. In experiments, the progress criterion does not seem to be a limitation in the applicability of the proof system. Some parts of this dissertation were also formalized in the proof assistant language Lean and thus allow the usage of the formalized proof rules to reason about concurrent and probabilistic programs in Lean.