Model checking technology arguably ranges among the foremost applications of logic to computer science and computer engineering. In the twenty-five years since its invention, model checking has achieved multiple breakthroughs, bridging the gap between theoretical computer science, hardware and software engineering. Today, model checking is extensively used in the hardware industry, and has become feasible for verifying many types of software as well. Model checking has been introduced into computer science curricula at universities worldwide, and virtually has become a universal tool for the analysis of systems.
As the number of research groups and conferences in model checking is steadily increasing, the symposium will focus on the state of the art and the future challenges in model checking, seen through the eyes of the leading researchers which have shaped the field during the last decades.
The symposium will consist of invited lectures delivered by leading researchers in the field of model checking. The invited speakers are encouraged to reflect the state of the art in their respective field of expertise, and to focus on the most important and exciting future research directions.
Orna Grumberg, Technion Haifa, Israel
Helmut Veith, Technische Universität München, Germany
List of speakers and short abstracts
OBDDs and DPLL-based checkers have very complementary strengths. OBDDs readily handle quantified Boolean formulas (QBF), whereas attempts to extend DPLL to QBF have had limited success. Some SAT problems that are completely intractable for DPLL are quite trivial with OBDDs. On the other hand, OBDDs cannot cope with problems that involve large numbers of variables, whereas SAT checkers are relatively insensitive to the number of variables. Despite many attempts, no one has found a way to combine the bottom-up approach of OBDDs with the top-down approach of DPLL. A successful hybrid of these two would have profound impact on symbolic model checking.
Game models are necessary to ask and answer certain important questions about systems. In particular, the problem of synthesizing a reactive system that satisfies a temporal specification is a problem of constructing a winning strategy. Other applications include compatibility checking for components, receptiveness and refinement checking for models, and test-case generation. Moreover, game models offer the flexibility to limit the knowledge of a player when making a choice, to allow a player probabilistic choices, and to combine the choices of different players in synchronous or asynchronous fashion. The precise formalization of a game will determine the difficulty of solving it. We survey classical and recent results on games with omega-regular winning conditions, as well as their applications in system design and verification.
In this talk we consider a stronger notion of translation, in which the automaton A_f, called the TEMPORAL OBSERVER of formula f, has a Boolean output variable x such that x=1 at position j of a sequence s iff (s,j) |= f. We will describe several advantages of the temporal observer construct. The construction of temporal observers is modular. That is, the temporal observer of a formula "f op g", where "op" can be any Boolean or temporal operator applied to arbitrary LTL formulas f and g, can be constructed by combining the temporal observers of f, g, and "op". As a result, we can outline a model-checking algorithm for LTL formulas which is compositional in the structure of the formula. This type of compositionality has been long considered to be a unique feature of CTL. Based on this approach to LTL model checking, we will present a compositional method for model-checking arbitrary CTL* formulas.
We will show how the notion of temporal testers is easily and naturally extended to deal with past formulas and many of the new operators introduced in the new hardware property specification language PSL. It can also be adapted to deal with versions of LTL which are evaluated over finite sequences as well as infinite sequences, as is often required in applications of testing and run-time verification.