10:30      Coffee and tagging

10:50      Abstraction Methods for Liveness

               Amir Pnueli, New York University and Weizmann Institute (Emeritus)

Abstract: It is a known fact that finitary state abstraction methods, such as predicate abstraction, are inadequate for verifying general liveness properties or even termination of sequential programs. In this talk we will present an abstraction approach called "ranking abstraction" which is sound and complete for verifying all temporally specified properties, including all liveness properties.

We will start by presenting a general simple framework for state abstraction emphasizing that, in order to get soundness, it is necessary to apply an over-approximating abstraction to the system and an under-approximating abstraction to the (temporal) property. We show that the finitary version of this abstraction is complete for verifying all safety properties. We then consider abstraction approaches to the verification of deadlock freedom, presenting some sufficient conditions guaranteeing that deadlock freedom is inherited from the concrete to the abstract.

Finally, we introduce the method of ranking abstraction and illustrate its application to the verification of termination and more general liveness properties. In this presentation we emphasize the similarity between predicate abstraction and its extension into ranking abstraction. In particular, we illustrate how abstraction refinement can be applied to ranking abstraction. Time permitting, we will present a brief comparison between ranking abstraction and the methods of transition abstraction developed by Podelski, Rybalchenko, and Cook which underlie the "Terminator" system.

Bio: Amir Pnueli is a Silver Professor of Computer Science at the Courant Institute of Mathematical Sciences at New York University, since 1999. Prof. Pnueli is the 1996 recipient of the ACM Turing award, and the 2000 recipient of the Israel prize in the category of Exact Sciences. In 2008, Pnueli received the 2007 Software System Award, as a member of the team that developed the software engineering tool Statemate.

Prof. Pnueli is mainly known for the introduction of temporal logic into Computer Science; his work on the application of temporal logic and similar formalisms for the specification and verification of reactive systems; the identification of the class of "Reactive Systems" as systems whose formal specification, analysis, and verification require a distinctive approach; and the development of a rich and detailed methodology, based on temporal logic, for the formal treatment of reactive system; extending this methodology into the realm of real-time systems; and more recently, introducing into formal analysis the models of hybrid systems with appropriate extension of the temporal-logic based methodology.

Beside his more theoretical work, concerning a complete axiom system and proof theory for program verification by temporal logic, he also contributed to algorithmic research in this area. He developed a deductive system for linear-time temporal logic and model-checking algorithms for the verification of temporal properties of finite-state systems. Together with David Harel, Pnueli worked on the semantics and implementation of Statecharts, a visual language for the specification, modeling, and prototyping of reactive systems. This language has been applied to avionics, transport, and electronic hardware systems. His current research interests involve synthesis of reactive modules, automatic verification of multi-process systems, and specification methods that combine transition systems with temporal logic.

11:30    Discriminative Model Checking

            Doron Peled, Bar-Ilan University

Abstract: Model checking typically compares a system description with a formal specification, and returns either a counterexample or an affirmation of compatibility between the two descriptions. Counterexamples provide evidence to the existence of an error, but it can still be very difficult to understand what the cause for this error is.

We propose a model checking methodology which uses two levels of specification. Under this methodology, we group executions as good} and bad with respect to satisfying a base LTL specification. We use an analysis specification, in CTL* style, quantifying over the good and bad executions. This specification allows checking not only whether the base specification holds or fails to hold in a system, but also how it does so. Some examples are checking whether one needs infinite number of scheduling decisions to reach a bad execution, or verifying the safety part of a property that does not itself hold for a system. We propose a model checking algorithm in the style of the standard CTL* decision procedure. This framework can be used for comparing between good and bad executions in a system and outside it, providing assistance in locating the design or programming errors.

12:10      Shape Analysis of Concurrent Programs

               Mooly Sagiv, TAU

Abstract: Shape analysis concerns the problem of automatically inferring shape invariants for programs that perform destructive updating on dynamically allocated storage. I will describe recent works in shape analysis of concurrent programs in order to prove that concurrent data structure implementations are correct.

Bio: Mooly Sagiv received his PhD from the Technion Israel in 1990. He was then a research staff member at IBM until 1994. In 1994 he did his Postdoc with Tom Reps at the University of Wisconsin. In 1997, he became a faculty member at TAU. More information is available at http://www.cs.tau.ac.il/~msagiv

12:50     Lunch

13:35     Compositional Verification and 3-Valued Abstractions Join Forces

              Orna Grumberg, Technion

Abstract: Model checking is an automated technique for the verification of hardware and software systems. It gets a description of a system by means of a state machine (graph). It also gets a specification given as a formula in some temporal logic. It returns "yes" if the system satisfies the specification and "no", otherwise.

Model checking has been successfully applied to verifying complex systems. However, its application to very large systems is limited due to its high space requirements.

Two of the most promising approaches to fighting the high space requirements are abstraction and compositional verification. In this work we join their forces to obtain a novel fully automatic compositional technique that can determine the truth value of the full Mu-calculus logic with respect to a given system.

In the talk we will give the needed background and describe our results.

Joint work with Sharon Shoham

Bio: Orna Grumberg received her B.Sc. (1976), M.Sc (1978) and Ph.D. (1984) from the Computer Science Department at the Technion – Israel Institute of Technology. Since 1984 she is a faculty member there. During 1985-1987 she held a postdoctoral position in Ed Clarke's Verification Group at Carnegie-Mellon University. Since then she spends every summer at CMU as a visiting researcher in this group. In 1992 she was on sabbatical in Bell Laboratories.

Her interests include model checking of hardware and software systems, abstraction-refinement, modularity, symmetry and vacuity in model checking, 3-valued abstraction-refinement, distributed model checking, SAT solvers, model checking games, and symbolic trajectory evaluation (STE).

Together with Ed Clarke and Doron Peled she is the co-author of the book "Model Checking'', published by MIT Press in 1999.

She is on the editorial board of Information and Computation and Formal methods in System Design. She served on numerous program committees of conferences and workshops. She chaired the Computed-Aided Verification (CAV) conference in 1997 and co-chaired the TACAS conference in 2007. She is on the directory board of the NATO summer school in Marktoberdorf (blue series).

14:15      Tarskian structures and languages in the study of concurrency

              Uri Abraham, Ben-Gurion University

Abstract: Whereas mathematicians argue and formulate their investigations in terms of Tarskian structures and languages, in Verification and Formal Specification research computer scientists rely on different approaches (such as temporal logic) which are amenable to machine checking. In this lecture I will argue that Tarskian structures have a place in the research of concurrency, mainly in that they can promote understanding at a formal level of complex phenomena that arise in that study.

Bio: Uri Abraham is a professor at the departments of mathematics and computer science at Ben Gurion. His main interests are in mathematical logic and set theory and in the study of concurrency. A question of main concern is finding a framework in which concurrent protocols can be specified and proved correct in such a way that the passage from the informal to the formal and back is made in the easier and most natural way for the human researcher.

14:55      Synthesis from Component Libraries

               Yoad Lustig, Student at Hebrew University of Jerusalem

Abstract: Synthesis is the automatic construction of a system from its specification. In the classical synthesis algorithms it is always assumed the system is "constructed from scratch" rather than "composed" from reusable components. This, of course, rarely happens in real life. In real life, almost every non-trivial commercial system, either in hardware or in software system, relies heavily on using libraries of reusable components. Furthermore, other contexts, such as web service orchestration, can be modeled as synthesis of a system from a library of components.

We define and study the problem of LTL synthesis from libraries of reusable components. We define two notions of composition: functional composition, for which we prove the problem is undecidable, and structural composition, for which we prove the problem is 2EXPTIME-complete. As a side benefit we derive an explicit characterization of the information needed by the synthesizer on the underlying components. This characterization can be used as a specification formalism between component providers and integrators.

Joint work with Moshe Y. Vardi

Bio: Yoad Lustig is a PhD Student of Prof. Orna Kupferman in the Computer Science Department at the Hebrew University of Jerusalem. He is now completing his thesis on the topic "Reasoning about lattice-based multi-valued systems". He received his B.Sc. in Mathematics from the Hebrew University of Jerusalem, and his M.Sc. in CS from the Weizmann Institute.

15:20    Coffee

15:35    Correctness and Interference-Freedom for Libraries of Reusable Aspects

            Shmuel Katz, Technion

Abstract: Aspects have become popular constructs for modularizing treatment of concerns that otherwise cross-cut object-oriented systems. In this talk, the specification of aspects is defined, and model checking is used to show correctness and interference-freedom among collections of reusable aspects.

Bio: Shmuel Katz is an Associate Professor in the Computer Science Department at the Technion, working on software verification, aspect-oriented programming, and software engineering. He also heads the Formal Methods Lab of the EU Network of Excellence AOSD-Europe, coordinating work on formal methods for aspect-oriented software development.

16:15    Self-* Programming: Run-Time RSR-Box Control Synthesis

            Olga Brukman, Student at Ben-Gurion University

Abstract: Real life situations may require an automatic fast update of the control of a plant, whether the plant is an airplane that needs to overcome an emergency situation due to drastic environment change, or a process that needs to continue executing an application in spite of a change in an operating system behavior. Settings for run-time control synthesis are defined, assuming the environment maybe totally dynamic, but is reentrant and history oblivious for long enough periods. A reentrant environment allows several copies of a plant to interact with the environment independently; a history oblivious environment ensures a repetition of an interaction (in the probabilistic case with the same probability) starting with a plant in a certain state and replaying its output to the environment.

Total dynamic changes of the environment do not allow a definition of weakly realizable specifications, as weakly realizable specifications depend on the environment behavior. On line experiments of the environment assists in the implementation of unrealizable specifications; automatically checking whether the unrealizable specifications define weakly realizable specifications, given the behavior restriction of the current environment. A successful search for a control implicitly identifies the weakly realizable specifications, and explicitly the implementation that respect the specifications.

Joint work with Shlomi Dolev

Bio: Olga recived her BSc (2001) and is about to graduate PhD from Computer Science Department in Ben-Gurion University under supervision of Prof. Shlomi Dolev.

16:40    On the Succinctness of Nondeterminism

            Binyamin Aminoff, Student at Hebrew University of Jerusalem

Abstract: Much is known about the differences in expressiveness and succinctness between nondeterministic and deterministic automata on infinite words. Much less is known about the relative succinctness of the different classes of nondeterministic automata. For example, while the best translation from a nondeterministic Büchi automaton to a nondeterministic co-Büchi automaton is exponential, and involves determinization, no super-linear lower bound is known. This annoying situation, of not being able to use the power of nondeterminism, nor to show that it is powerless, is shared by more problems, with direct applications in formal verification.

In this talk I will present a family of problems of this class. The problems originate from the study of the expressive power of deterministic Büchi automata: Landweber characterizes languages L of infinite words that are recognizable by deterministic Büchi automata as those for which there is a regular language R (of finite words) such that L is the limit of R; that is, an infinite word w is in the language L if and only if it has infinitely many prefixes in R. Two other operators that induce a language of infinite words from a language of finite words are co-limit, where w is in L if and only if w has only finitely many prefixes in R, and persistent-limit, where w is in L if and only if almost all the prefixes of w are in R. Both co-limit and persistent-limit define languages that are recognizable by deterministic co-Büchi automata. They define them, however, by means of nondeterministic automata. For the three limit operators, the deterministic automata for R and L share the same structure. It is not clear, however, whether and how it is possible to relate nondeterministic automata for R and L, or to relate nondeterministic automata to which different limit operators are applied. It turns out that the situation is involved: in some cases we are able to describe a polynomial translation, whereas in some we present an exponential lower bound.

Joint work with Orna Kupferman