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. We show two applications of this result: to under-approximate the reachable state space of multi-threaded procedural programs, and to under-approximate the reachable state space of counter automata with context-free constraints.