Abstract:
Many program analyses can be reduced to reachability problems. A program state, defined by a predicate over program control and data, is reachable if an input exists that causes program execution to reach the designated control location with variable values that satisfy the designated data constraints. While powerful, this framework is unable to answer a range of valuable quantitative questions about program behavior. For example, if one could determine how many inputs could reach a resource-intensive statement then one could perform a kind of static performance analysis.

Motivated by a desire to analyze probabilistic simulation models in the field of individual-based Ecology, we enhanced symbolic execution to incorporate logical model counting algorithms. This exposed several scalability challenges that have led, over the years, to improvements in the performance of symbolic execution itself. We developed a general probabilistic symbolic execution (PSE) framework with several applications in mind, but in the intervening years a number of other researchers have significantly broadened its applicability to a range of quantitative program analyses including: program complexity analysis, the detection of algorithmic and side-channel attacks, forms of static performance and reliability analysis, and measures of program similarity.

In this talk we describe our motivation for developing PSE, the technical obstacles we overcame to develop a workable PSE framework, a range of applications of PSE, and offer some thoughts on the future of quantitative program analysis.

Speaker Biography:
Matthew B. Dwyer is the Robert Thomson Distinguished Professor in the Department of Computer Science at the University of Virginia. He has authored more than 140 scholarly publications in program analysis, software specification, and automated formal methods. His research contributions have been recognized with the ICSE “Most Influential Paper” award (2010), the SIGSOFT “Impact Paper” award (2010), the ESEC/FSE “Test of Time” award (2018), the SIGSOFT “Impact Paper” award (2021). He was named a Fulbright Research Scholar (2011), an IEEE Fellow (2013), a Parnas Fellow (2018), and an ACM Fellow (2019), and has received the IEEE Computer Society Harlan D. Mills Award (2022).