Advanced Querying for Property Checking
Nicholas Kidd, Akash Lal, Thomas Reps · Minds at UW (University of Wisconsin) · 2007
Abstract. Extended weighted pushdown systems (EWPDSs) are an ex-tension of pushdown systems that incorporate infinite-state data abstrac-tions. Nested-word automata (NWAs) are able to recognize languages that exhibit context-free properties, while retaining many of the decid-ability properties of finite automata. We study property checking of pro-grams where the program model is an EWPDS and the property is spec-ified by an NWA. We show how to combine an NWA A with an EWPDS E to create an EWPDS EA such that reachability analysis on EA checks property A on program E. This construction allows us to retain the ca-pability of running advanced queries on programs modeled as EWPDSs, such as the ability to (i) find all program nodes that lie on an error path (via error projections); and (ii) answer context-bounded reachabil-ity queries for concurrent programs with infinite-state abstractions (via context-bounded model checking). 1