As software systems become more and more pervasive and sophisticated, their vulnerabilities are exploited at increasingly worrisome speeds. Static analysis can detect a variety of flaws, including different security-related issues, at an early stage in the software development process.

We introduce the topic by discussing different perspectives, from increased lawmaker awareness and upcoming bureaucratic regulations, to coding standards and vulnerability databases.

We then focus on the problem of data race detection with a novel static technique for C programs with POSIX threads. The key element of the technique is a reduction to reachability that can be combined with bounded model checking and context-bounded analysis for great detection accuracy.

This talk includes joint work with Emerson Sales, Emilio Tuosto, and Rocco De Nicola.

Bio: Omar Inverso is a tenure-track assistant professor at the Gran Sasso Science Institute in L’Aquila, Italy. His research interests include formal languages and methods, software verification, static analysis, and decision procedures, with applications to concurrent software, distributed systems, and complex systems in general.