Collaborative Research: SHF: Medium: Probabilistic Concurrent Outcome Logic (pcOL) -- Expressive Specifications for Concurrent Randomized Programs

Software bugs can have disastrous consequences, ranging from financial costs to loss of human life. As a result, for high-stakes systems, software vendors are increasingly applying techniques that can prove the absence of various kinds of bugs. However, existing techniques have limitations that make them inapplicable for certain types of programs that make use of randomness, which is common in sensitive software domains such as cryptography and machine learning. This project will develop new techniques for reasoning about randomness in programs, which will make it possible to prove important properties about these programs, thereby improving software quality in these critical areas. In addition, the team of researchers will develop educational materials to make the project's ideas more broadly accessible to students, researchers, and industrial practitioners. This project targets programs that exhibit two important kinds of effectful features: concurrency and randomization. Existing formal verification techniques cannot handle the complexity and expressivity of many programming language features, and these features make it harder to write, test, and reason about programs. Establishing correctness in the presence of just one of these features is hard enough, and it only becomes more difficult when they are combined. This project will develop program logics and reasoning tools that can enable more precise, compositional analysis of concurrent randomized programs by building on a new semantic model of randomness and concurrency. The investigators will formally verify the soundness of the logic and build a framework for using it inside of an interactive theorem prover. This formalized framework will facilitate further breakthroughs in verification of concurrent randomized programs in different domains. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.