Modern-day software is increasingly complex and software engineering is commonly accepted as a challenging, error-prone task. Consequently, software bugs are prevalent, incurring detrimental financial costs and often risking human lives. Program analyses provide rigorous and effective means to automated bug detection, and are becoming an integral part of the software development process. In this talk, I will present recent algorithmic advances in two impactful domains of program analysis: (i) static analysis and (ii) stateless model checking.

Static analyses are lightweight approximations to program behavior and largely constitute the first step to bug detection in the software development process. In the first part, I will introduce the Algebraic Path Problem on Recursive Graphs (APP) and its close variant of Dyck Reachability (DR). These problems serve as algorithmic formulations of static analyses on various domains, such as dataflow/alias/data-dependence analysis and program slicing. I will present new algorithms for APP and DR based on the graph-theoretic notion of treewidth, that lead to theoretical complexity improvements and provide a significant scalability boost in practice.

Stateless model checking is one of the most influential techniques in the analysis of concurrent programs because of its effectiveness in dealing with the state-explosion problem. In the second part, I will present Dynamic Partial Order Reduction (DPOR), a widespread stateless technique for model checking concurrent programs. I will outline some foundational limitations to existing DPOR approaches, and introduce a new abstraction of concurrent semantics, called the Observation Equivalence (OE), which overcomes some of these limitations. I will demonstrate algorithmic applications of OE in two domains: (i) stateless model checking and (ii) dynamic race detection.