Abstract: In this talk, we will be exploring techniques for automatically checking concurrency properties in programs. Some of the current techniques (like Java Pathfinder) systematically control thread scheduling, which forces different interleavings of concurrent threads to be explored in order to reveal concurrency bugs such as race conditions and deadlocks, while others use more specialized and efficient analyses that target only certain classes of bugs, such as the Java Deadlock Analyzer.
In our work, we encode the concurrent behavior of programs into state machines called Petri nets, which naturally model concurrent systems and can also represent unbounded behaviors of programs, such as unbounded thread creation or unbounded resource usage. PETRIFY’s Petri net encoding is succinct, allowing efficient reasoning even as program complexity grows.

Chair: Giuseppe Crupi