| Abstract |
Many problems in the verification of concurrent software
systems reduce to checking the non-emptiness of the intersection of
two context-free languages, an undecidable problem. We propose a
decidable under-approximation, and a semi-algorithm based on the
under-approximation, for this problem through bounded languages, which
are context-free subsets of a regular language of the form w_1*w_2*...
w_k* for some w_1,...,w_k in Sigma*. Bounded languages have nice
structural properties, in particular the non-emptiness of the
intersection of a bounded language and a context free language is
decidable.
Our main theoretical result is a constructive proof of the following
result: for any context free language L, there is a bounded language
L' included in L which has the same Parikh image as L. Along the way,
we show an iterative construction that associates with each context
free language a family of linear languages and linear substitutions
that preserve the Parikh image of the context free language. As an
application of this result we show how to under-approximate the
reachable state space of multi-threaded procedural programs.
Pierre Ganty is research professor at the public research institute IMDEA Software in
Madrid, Spain. He joined IMDEA in September 2009 after completing his postdoc
at the University of California, Los Angeles (UCLA). He holds a PhD in Computer
Science from the University of Brussels, Belgium and from the
University of Genova,
Italy and has co authored papers with outstanding researchers in computer
science like Patrick Cousot from ENS (Paris), Javier Esparza from TU Munchen
(Germany) and Rupak Majumdar from UCLA (USA).
|
