Advanced Querying for Property Checking
File(s)
Date
2007Author
Kidd, Nicholas
Lal, Akash
Reps, Thomas
Publisher
University of Wisconsin-Madison Department of Computer Sciences
Metadata
Show full item recordAbstract
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).
Permanent Link
http://digital.library.wisc.edu/1793/60606Citation
TR1621