Home | Search | Help  
Home Page Università di Genova

Seminar Details


Date 12-2-2010
Time 11:00
Room/Location DISI-Sala conferenze
Title Bounded Underapproximations
Speaker Dr. Pierre Ganty
Affiliation IMDEA Software, Madrid, Spain
Link https://www.disi.unige.it/index.php?eventsandseminars/seminars
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).

Back to Seminars