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