The set constraint/CFL reachability connection in practice

Many program analyses can be reduced to graph reachability problems involving a limited form of context-free language reachability called Dyck-CFL reachability. We show a new reduction from Dyck-CFL reachability to set constraints that can be used in practice to solve these problems. Our reduction is much simpler than the general reduction from context-free language reachability to set constraints. We have implemented our reduction on top of a set constraints toolkit and tested its performance on a substantial polymorphic flow analysis application. Categories and Subject Descriptors D.2.4 [Software Engineering]: Software/Program Verification; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages General Terms Algorithms, Design, Experimentation, Languages, Theory Keywords Set constraints, context-free language reachability, flow analysis, type qualifiers

• Type: Conference
• Year: 2004
• Where: PLDI
• Authors: John Kodumal, Alexander Aiken
• Keywords: Context-free Language Reachability, Dyck-CFL Reachability, PLDI 2004, Programming Languages, Reachability Problems