Message-ID: <4E06A937DADC3842ACE4D3A1096A9EAC03843F@JANUS.eecs.berkeley.edu> From: George Necula <necula@EECS.Berkeley.EDU> Subject: PS seminar today Date: Mon, 15 Oct 2001 09:22:24 -0700 Please join us at the Programming Systems seminar at 4pm in Soda 310. Patrice Godefroid (best known for developing the Verisoft model-checking toold for software) from Bell Labs will give a talk on 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
This archive was generated by hypermail 2b30 : 11/04/02 PST