Language Theoretic CEGAR

Title:Language Theoretic CEGAR
Speaker:Zhenyue Long
Time: 10:00am, November 29th (Tuesday), 2011
Venue:Lecture Room, Level 3, Building No. 5, 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.