Abstract 
Many problems in the verification of concurrent software
systems reduce to checking the nonemptiness of the intersection of
two contextfree languages, an undecidable problem. We propose a
decidable underapproximation, and a semialgorithm based on the
underapproximation, for this problem through bounded languages, which
are contextfree 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 nonemptiness 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 underapproximate the
reachable state space of multithreaded 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).
