Bounded underapproximations

Pierre Ganty 1 Rupak Majumdar 2 Benjamin Monmege 3, 4
4 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : We show a new and constructive proof of the following language-theoretic result: for every context-free language L, there is a bounded context-free language L'⊆L which has the same Parikh (commutative) image as L. Bounded languages, introduced by Ginsburg and Spanier, are subsets of regular languages of the form w1*w2*... wm* for some w1,...,wm∈ Σ*. In particular bounded context-free languages have nice structural and decidability properties. Our proof proceeds in two parts. First, we give a new construction that shows that each context free language L has a subset LN that has the same Parikh image as L and that can be represented as a sequence of substitutions on a linear language. Second, we inductively construct a Parikh-equivalent bounded context-free subset of LN. We show two applications of this result in model checking: to underapproximate the reachable state space of multithreaded procedural programs and to underapproximate the reachable state space of recursive counter programs. The bounded language constructed above provides a decidable underapproximation for the original problems. By iterating the construction, we get a semi-algorithm for the original problems that constructs a sequence of underapproximations such that no two underapproximations of the sequence can be compared. This provides a progress guarantee: every word w∈L is in some underapproximation of the sequence, and hence, a program bug is guaranteed to be found. In particular, we show that verification with bounded languages generalizes context-bounded reachability for multithreaded programs.
Type de document :
Article dans une revue
Formal Methods in System Design, Springer Verlag, 2012, 40 (2), pp.206-231. 〈10.1007/s10703-011-0136-y〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00776791
Contributeur : Benedikt Bollig <>
Soumis le : mercredi 16 janvier 2013 - 11:16:05
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Identifiants

Collections

Citation

Pierre Ganty, Rupak Majumdar, Benjamin Monmege. Bounded underapproximations. Formal Methods in System Design, Springer Verlag, 2012, 40 (2), pp.206-231. 〈10.1007/s10703-011-0136-y〉. 〈hal-00776791〉

Partager

Métriques

Consultations de la notice

88