Property-Directed k-Reachability

Klaus Draeger

We apply the recently introduced Property-Directed Reachability (POR) approach to the problem of k-reachability, i.e. the question whether a program can reach at least k observably different states from the same visible inputs. This problem arises in contexts like data-flow analysis, where a positive answer to the 2-reachability question indicates an information leak from confidential inputs. Current methods for this problem are limited to bounded analysis, and require inflating the set of variables, with a corresponding increase of complexity; we find that POR is a natural fit for this question, since it has neither of these problems.

Joint work with Pasquale Malacaria and Michael Tautschnig.