Static Analysis of Programs with Low Tree-Width

8^th November 2018, 13:00
Rasmus Ibsen-Jensen

Abstract

Static analysis of programs is one of the main and most direct applications of verification, typically done without any assumption on the programs.
However, if a method is written without (or even with a few) GOTO statements, then, in many common programming languages, the control flow graph of the method have small constant tree-width. GOTO statements have in essence been taboo since a famous letter by Dijkstra in '68 and are thus extremely rarely used.

In this talk we exploit this property of programs to give faster algorithms for static analysis. Specifically, the talk will cover improved algorithms for programs of multiple methods and of concurrent, single methods, when the methods each have constant tree-witdh, based on my papers in POPL `15 and `16 and ongoing research.