About This Item

Ask the MINDS@UW Librarian

Advanced Querying for Property Checking

Show full item record


Kidd, Nicholas; Lal, Akash; Reps, Thomas
University of Wisconsin-Madison Department of Computer Sciences
Mar 15, 2012
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
Export to RefWorks 

Part of

Show full item record

Search and browse


Deposit materials

  1. Register to deposit in MINDS@UW
  2. Need deposit privileges? Contact us.
  3. Already registered? Have deposit privileges? Deposit materials.