Academic
Publications
Model-Checking Pushdown Systems

Model-Checking Pushdown Systems,Stefan Schwoon

Model-Checking Pushdown Systems   (Citations: 84)
BibTex | RIS | RefWorks Download
Published in 2002.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...One possibility is to use Schwoon’s BDD-based PDS techniques [24]; these represent the transitions of a PDS’s control-state from one configuration to another as a relation, using BDDs...

    Nicholas Kiddet al. A decision procedure for detecting atomicity violations for communicat...

    • ...This is different from a BPDS model used in software verification [2], where BA only monitors the state transitions of the Pushdown System (PDS) (see Related Work)...
    • ...This approach was improved by Schwoon [2], which results in a tool, Moped, for checking LTL properties of PDS...
    • ... be computed by exploiting the fact that a head � p, γ� is repeating and the repeating path satisfies the BPDS loop constraint iff � p, γ� is part of a Strongly Connected Component (SCC) of G and this SCC has internal edges labeled by (1, ∗, ∗), (∗,1, ∗) ,a nd(∗, ∗,1) ,w here∗ represents 0 or 1. Algorithm REPHEADS takes B 2 P as the input and computes the set R .R EPHEADS first utilizes the backward reachability analysis algorithm of [2], ...
    • ...forward reachability algorithm [2] with a complexity of O((|P |+|ΔB2P |) 3 ). Therefore, the LTL model checking of BPDS has the complexity of O((|P | + |ΔB2P |) 3 )...
    • ...The implementation is based on the Moped model checker [2]...

    Juncao Liet al. Model Checking Büchi Pushdown Systems

    • ...Pushdown systems [6], [7] additionally have an unbounded stack...

    Ajay Chanderet al. Optimal Test Input Sequence Generation for Finite State Models and Pus...

    • ...Pushdown Model Checking: This part performs pushdown model checking using MOPED [20] model checker which accepts pushdown system as input model...

    Hsin-Hung Linet al. Automated Adaptor Generation for Services Based on Pushdown Model Chec...

    • ...In this section, we provide a new enforcement for the where-security based on reachability analysis of symbolic pushdown system [20]...

    Cong Sunet al. A new enforcement on declassification with reachability analysis

Sort by: