Message-ID: <4E06A937DADC3842ACE4D3A1096A9EAC0383B3@JANUS.eecs.berkeley.edu> From: George Necula <necula@EECS.Berkeley.EDU> Subject: Patrice Godefroid visit and talk next Monday Date: Mon, 8 Oct 2001 12:18:11 -0700 Hi all, Patrice Godefroid will visit us and will give a talk on his recent work on software model checking. The talk is on Monday, October 15 at 4pm in Soda 310. The title and the abstract are below. He will be here the whole day on Monday and he will be happy to meet with people. Please let me know if you'd like to meet him. I have just learned that Sriram Rajamani from Microsoft Research will also be visiting on the same day. He would very much like to talk to people about a result they have. I asked him if he can stay on Tuesday as well but if now I hope that people will make an effort to meet with Sriram as well. George. Title: Generalized Model Checking: Theory and Applications Abstract: Generalized model checking is a framework for reasoning about partial state spaces of concurrent reactive systems. The state space of a system is only "partial" (partially known) when a full state-space exploration is not computationally tractable, or when abstraction techniques are used to simplify the system's representation. In this talk, we present the main ideas and key notions behind this framework, namely models for partial state spaces (partial Kripke structures and Modal Transition Systems), completeness preorders (to measure the level of completeness of a partial state space), 3-valued temporal logic (properties of partial state spaces evaluate to either true, false or unknown), generalized model checking (given a partial state space and a temporal property, does there exist a more complete state space that satisfies the property?), and algorithms and complexity bounds for both the traditional and generalized model-checking problems for various temporal logics. We then discuss applications. Specifically, we show how generalized model checking can extend existing automatic abstraction techniques (such as predicate abstraction) for model checking concurrent/reactive programs and yield the three following improvements: (1) any temporal logic formula can be checked (not just universal properties as with traditional conservative abstractions), (2) verification results are guaranteed to be both complete AND sound, and (3) verification results can be more precise for the same cost in the size of the partial state space (program). Joint work: this talk includes results from two papers with Glenn Bruns presented at CAV'99 and CONCUR'2000, and a paper with Radha Jagadeesan and Michael Huth presented at CONCUR'2001. ----------------------------------------------------------------------- Patrice Godefroid Bell Laboratories, Lucent Technologies Room 2A-306 263 Shuman Blvd Naperville, IL 60566, U.S.A. Email: god@bell-labs.com
This archive was generated by hypermail 2b30 : 11/04/02 PST