Advanced Querying for Property Checking

Abstract

Extended weighted pushdown systems (EWPDSs) are an extension of pushdown systems that incorporate infinite-state data abstractions. Nested-word automata (NWAs) are able to recognize languages that exhibit context-free properties, while retaining many of the decidability properties of finite automata. We study property checking of programs where the program model is an EWPDS and the property is specified by an NWA. We show how to combine an NWA A with an EWPDS E to create an EWPDS E' such that reachability analysis on E' checks property A on program E. This construction allows us to retain the capability 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 reachability queries for concurrent programs with infinite-state abstractions (via context-bounded model checking).