CS Colloquium - Joseph Tassarotti
Refreshments available at 3:45
Hosts: Zhong Shao and Ruzica Piskac
Title: Verifying Concurrent Randomized Programs
Abstract:
In recent years, multiple realistic software systems have been formally verified, including microkernels, filesystems, and cryptographic primitives. Despite these successes, many fundamental data structures and algorithms remain difficult to verify. Challenges arise when programs use concurrency or randomization because such programs behave non-deterministically. Although many specialized logics have been developed to reason about programs that use concurrency or randomization, most can only handle the use of one of these two features in isolation. However, many common concurrent data structures also use randomization, making it important to consider the combination.
I will discuss how I have devised a logic to reason about programs that are both concurrent and randomized by embedding a probabilistic logic into a concurrent one. Afterward, I will describe future applications of this work to the verification of machine learning systems, motivated by my experience in a separate line of work developing scalable inference algorithms for such systems.
Bio:
Joseph Tassarotti is a postdoctoral associate in the Parallel and Distributed Operating Systems group at MIT. He recently received his Ph.D. from Carnegie Mellon University, where he was advised by Robert Harper. Previously, he was an intern at MPI-SWS, INRIA, and Oracle Labs. Joseph is the recipient of an NDSEG fellowship. He obtained a Bachelor’s degree from Harvard University in 2013.