Title: Language Theoretic CEGAR

Speaker: Zhenyue Long (Phd Student, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences)

Time: 10:00am, November 29th (Tuesday), 2011.

Venue: Lecture Room, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Abstract:

We give a language-theoretic counterexample-guided abstraction refinement (CEGAR) algorithm for the safety verification of concurrent recursive programs. Using a standard reduction, we reduce the safety verification problem to the (undecidable) language emptiness problem for the intersection of context-free languages. Initially, our CEGAR procedure overapproximates the intersection by a context-free language. If the overapproximation is empty, we declare the system safe. Otherwise, we compute a ''bounded language'' from the over-approximation and check the emptiness of the intersection of the context free languages and the bounded language (which is decidable). If the intersection is non-empty, we report a bug. If empty, we refine the overapproximation by removing the bounded language and try again. We give concrete algorithms to approximate context-free languages using regular languages and to generate bounded languages representing a family of counterexamples. Based on the algorithms, we have implemented a model checker named LCegar, and we provide an experimental comparison on various choices for the regular overapproximation and the bounded underapproximation.