Advanced Querying for Property Checking
Nicholas Kidd, Akash Lal, and Thomas Reps
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).
(Click here to access the paper:
PDF.)
University of Wisconsin