This talk will describe our recent research on simplifying concurrent programming by automatically synthesizing synchronization protocols for "implicit monitors”, a convenient programming abstraction that serves as a specification of shared-memory concurrent programs. Given a high-level (non-executable) implicit-monitor specification with no locks or signaling operations, our approach automatically synthesizes an executable implementation that is both efficient and correct-by-construction. Our method infers all signaling operations that are needed to prevent deadlocks and introduces fine-grained locking to ensure atomicity and data-race-freedom while maximizing parallelization opportunities. The talk will showcase how we can leverage a combination of program verification, maximum satisfiability (MaxSAT), and static analysis to make the synthesis of such efficient concurrent programs feasible.

Isil Dillig is an Associate Professor of Computer Science at the University of Texas at Austin where she leads the UToPiA research group. Her main research area is programming languages, with a specific emphasis on static analysis, verification, and program synthesis. The techniques developed by her group aim to make software systems more reliable, secure, and easier to build in a robust way. Dr. Dillig is a Sloan Fellow and a recipient of the NSF CAREER award. She obtained all her degrees (BS, MS, and PhD) from Stanford University.