A general class of program analyses area combination of context-free and regular language reachability. We define  regularly annotated set constraints , a constraint formalism that captures this class. Our results extend the class of reachability problems expressible naturally in a single constraint formalism, including such diverse applications as interprocedural dataflow analysis, precise type-based flow analysis, and pushdown model checking.
['John Kodumal', 'Alex Aiken']
Regularly annotated set constraints