

FLoC MEETINGS PROGRAM FACILITIES SEATTLE ORGANIZATION MISCELLANEOUS OUTOFDATE 
25MC on Wednesday, August 16thSession (09:00‑10:30)
Break (10:30‑11:00)Session (11:00‑12:30)
25MC Lunch/Panel (12:30‑14:00)

14:00‑14:30  Thomas Henzinger
(EPFL Lausanne & UC Berkeley) From Graph Models to Game Models [ppt] A model that preserves the individuality of multiple actors in a transition system is a game model. The resulting game is played on the state space of the system. The players represent different processes of the system, or the environment. In a given state, the choices made by the players determine the successor state. Some of the players may compete, others collaborate, with the objective of satisfying a temporal specification. A graph model (or Kripke structure) is the special case of a game model where there is only a single player (who resolves nondeterminism). Game solving, therefore, is the generalization of model checking to two or more players. 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 testcase 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 omegaregular winning conditions, as well as their applications in system design and verification. 
14:30‑15:00  Limor Fix
(Intel Pittsburgh) Accelerating the Industrial Deployment of ModelChecking for SW Verification: Lessons from 10 years of ModelChecking Deployment for HW Verification in Intel [ppt] Model checking technologies have been applied to hardware verification in the last 15 years. Pioneering work has been conducted by Intel since 1990 using model checking technologies to build industrial hardware verification systems. This talk will review the evolution and the success of these systems in Intel and in particular it will focus on the many challenges and learning that have resulted from changing how hardware validation is performed in Intel to include formal verification. The talk will also include a discussing of how the learning from hardware verification can be used to accelerate the industrial deployment of modelchecking technologies for software verification. 
15:00‑15:30  Randy Bryant
(Carnegie Mellon University) A View from the Engine Room: Computational Support for Symbolic Model Checking [ppt] Symbolic model checking arose from the marriage of a Booleanlevel representation of the modelchecking task with a computational engine that supported the required set of operations. Ordered Binary Decision Diagrams (OBDDs) were the first approach with the necessary combination of efficiency and expressive power. More recently, Boolean satisfiability (SAT) checkers based on the DavisLogemanLoveland (DLL) algorithm have greatly extended the reach of bounded model checkers. OBDDs and DLLbased checkers have very complementary strengths. OBDDs readily handle quantified Boolean formulas (QBF), whereas attempts to extend DLL to QBF have had limited success. Some SAT problems that are completely intractable for DLL 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 bottomup approach of OBDDs with the topdown approach of DLL. A successful hybrid of these two would have profound impact on symbolic model checking. 
16:00‑16:30  Ken McMillan
(Cadence Berkeley) The Evolution of Symbolic Model Checking [ppt] This talk will trace the evolution of symbolic model checking over nearly two decades. We will note several general trends. In the early years the emphasisis was on increasingly sophisticated representations and image computation methods. This includes various generalizations, such as regular model checking, and a proliferation of methods for Boolean quantifier elimination. More recently, the trend has been toward approximate fixed point computations, which in effect allow us to prove weaker properties of larger systems. This has resulted in a synthesis of symbolic model checking and abstract interpretation. Still, given all this progress it is surprising to find BDDbased symbolic model checking at the heart of many modern systems. 
16:30‑17:00  Moshe Y. Vardi
(Rice University, Houston) From Church and Prior to PSL [pdf] One of the surprising deveopments in the area of program verification is how ideas introduced originally by Prior in the 1950s ended up yielding by 2004 an industrialstandard propertyspecification language called PSL. This development was enabled by the equally unlikely transformation of mathematical machinery, inroduced by Buechi in the early 1960 for secondorder number theory, into effective algorithms for model checking tools. This talk will attempt to depict the tangled skein of this development. 
17:00‑17:30  Amir Pnueli
(Weizmann Institute and New York University) The Merits of Temporal Testers: Transducers Compose while Acceptors Do Not [pdf] A central component in model checking temporal properties of finitestate systems is the translation of an LTL formula into a finitestate Omega automaton. According to the standard translation, automaton A corresponds to LTL formula f if the set of sequences accepted by A is precisely the set of sequences that satisfy f. This implies that the correspondence between A and f is required only at the initial position of each sequence. 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 modelchecking 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 modelchecking 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 runtime verification. 