Amir Pnueli, on the occasion of being awarded the Israel Prize in 2000
(Photo by © Dan Porges / Photo Shwartz)
Amir Pnueli Memorial Symposium
Amir Pnueli was one of the most influential computer scientists of our time. He
published more than 250 papers, many of them groundbreaking, including the 1977
paper, The Temporal Logic of Programs for which he won the 1996 ACM Turing
Award, the highest honor that can be received by a computer scientist.
On November 2, 2009, Amir unexpectedly passed away. His loss is felt deeply by
friends and colleagues around the world.
The Amir Pnueli Memorial
Symposium, held at New York University on May 89, 2010, convened a highly distinguished set of invited speakers to
revisit and build upon the ideas which inspired and defined his life's work. In order to document and broaden the impact of this historic meeting, the talks were videotaped and are
available, together with the accompanying slides, from the links below.
Schedule
May 8

08:15 AM  Welcome

08:30 AM  David Harel
 Can we Verify an Elephant? [slides  video]

09:00 AM  Krzysztof Apt
 Juggling using Temporal Logic [slides  video]
We explain the use of temporal logic in a study of infinite
simulations concerned with contingencies such as time, space, shape,
size, abstracted into a finite set of qualitative relations.
We implemented this approach in the constraint programming system
Eclipse by drawing on the ideas from bounded model checking. We
illustrate it by discussing a simulation of juggling.
This is a joint work with Sebastian Brand.

09:30 AM  Krishna Palem
 The Arrow of Time Through the Lens of Computing [video]
The concepts of temporal logic were introduced by Amir Pnueli into the
realm of computer science in general and programs in particular, to great
effect. Given a program specification, a crucial element of reasoning
through temporal logic is our ability to assert that one program event
occurs before or after the other, with an order intuitively rooted in our
notion of “time”. In the realm of temporal logic, such assertions are
abstracted as pure mathematical facts. An alternative is to consider the
physical realization by executing the specified program through, for
example, a microprocessorbased system. In such a case, a mechanism is used
to ensure that the desired temporal relationships from the program
specification are obeyed, and quite often, such a mechanism takes the form
of a clock. In physical instantiations however, such mechanisms have an
associated energy cost and are guided by the laws of physics in general and
thermodynamics in particular, with which the arrow of time and the
associated irreversibility are intimately intertwined. Viewed through this
lens, a key question arises whether the need for ensuring that the temporal
norms needed for program correctness accrue an inevitable energy cost. In
this talk, we sketch some of the intricacies underlying this question, and
we will hint at the subtle interactions between models of computing, time as
it is represented in them, and the associated thermodynamic cost attributes.
Amir in his early work relied as much on the philosophy of reasoning about
time as on the technical intricacies of mathematical logic. In recognition
of the richness of his intellectual endeavor, in this exposition, we adopt a
philosophical style mimicking that of the ancient Greek philosopher Zeno.

10:00 AM  Break

10:30 AM  Egon Börger
 Ambient Abstract State Machines with Applications [slides  video]
We define a simple and flexible abstract ambient concept which turned out to support current
programming practice, in fact can be instantiated to apparently all environment paradigms in use
in frameworks for distributed computing with heterogeneous components. For the sake of
generality and to also support rigorous highlevel system design practice we give the definition in
terms of Abstract State Machines (ASMs). Their most general notion of state allows one to fully
exploit the power of parameterization for defining an arguably most general abstract notion $\AMB
exp \IN M $ of machines working in a given environment. We show the definition to uniformly
capture the common static and dynamic disciplines for isolating states or run behavior as well as
for sharing memory, numerous wellknown patterns of objectoriented programming (e.g. for
subclassing, encapsulation, delegation, views), but also Cardelli's and Gordon's ambient calculus
for mobile agents. Joint work with Antonio Cisternino and Vincenzo Gervasi.

11:00 AM  Manfred Broy
 Realizability of System Interface Specifications [slides  video]

11:30 AM  Ofer Strichman
 Proving Equivalence between Similar Programs: a Progress Report [slides  video]

12:00 PM  Giora Slutzki
 Inverting Proof Systems for Secrecy under OWA [slides  video]

12:30 PM  Lunch

02:00 PM  Robert Kurshan
 VerificationGuided Hierarchical Design [slides  video]
Amir Pnueli was a forceful early proponent of deductive
reasoning as a basis for program verification. In the early
years, this appeared to be in conflict with automated verification
(primarily model checking). Yet over time, these two directions
have been found to be complementary, not antagonistic.
Today deductive elements such as compositional reasoning are essential
to mainstream model checking and algorithmic
drivers of deductive reasoning: preeminently, automatic proof
extraction in the context of SAT solving are prevalent.
I will describe how abstractionbased deductive reasoning is being
combined with model checking to provide a means for exploiting
design hierarchy to overcome performance and capacity limitations
in the software verification tools of the Electronic Design Automation
industry.

02:30 PM  Werner Damm
 Towards Component Based Design of Hybrid Systems [slides  video]
We propose a library based incremental design methodology
for constructing hybrid controllers from a component library of models
of hybrid controllers, such that global safety and stability properties
are preserved. To this end, we propose hybrid interface specifications of
components characterizing plant regions for which safety and stability
properties are guaranteed, as well as exception mechanisms allowing safe
and stabilitypreserving transfer of control whenever the plant evolves
towards the boundary of controllable dynamics. We then propose a composition
operator for constructing hybrid automata from a library of such
precharacterized components supported by compositional and automatable
proofs of hybrid interface specifications.

03:00 PM  Ken McMillan
 Invisible Invariants: Underapproximating to Overapproximate [slides  video]
In 2001, Pnueli and his coworkers introduced a method they called
"invisible invariants". This technique produces proofs of parameterized
or infinitestate systems, essentially by generalizing the proof of a
finite instance. The method is both surprising and subtle: surprising
in that it successfully produces overapproximations by
underapproximating, and subtle because it produces a parameterized
proof while performing only standard operations of finitestate model
checking. I'll describe the method in terms of abstract interpretation, and
relate it to other infinitestate methods, such as indexed predicate
abstraction and shape analysis.

03:30 PM  Break

04:00 PM  Allen Emerson
 Time for Time [slides  video]

04:30 PM  Leslie Lamport
 Temporal Logic: The Lesser of Three Evils [slides  video]

05:00 PM  Stephan Merz
 A Mechanized Proof System for TLA+ Specifications [slides  video]

May 9

08:30 AM  Moshe Vardi
 From Löwenheim to Pnueli, from Pnueli to PSL and SVA [slides  video]
One of the surprising developments in the area of program verification is how ideas introduced by
logicians in the first part of the 20th century ended up yielding at the start of the 21st century
industrystandard propertyspecification languages called PSL and SVA. Amir Pnueli played a key
role in this development. This talk attempts to trace the tangled threads of this story.

09:00 AM  Tom Henzinger
 Quantitative Modeling and Verification [slides  video]

09:30 AM  Patrick Cousot
 A Scalable Segmented Decision Tree Abstract Domain [video]

10:00 AM  Break

10:30 AM  Oded Maler
 Properties and Verification in the Continuous Domain [slides  video]

11:00 AM  Roni Rosner
 The Challenge of Evolutionary Verification [slides  pdf  video]

11:30 AM  Javier Esparza
 Newtonian Program Analysis: Solving Sharir and Pnueli's Equations [slides  video]

12:00 PM  Nir Piterman
 pAutomata: New Foundations for DiscreteTime Probabilistic Verification [slides  video]
We develop a new approach to probabilistic verification by adapting
notions and techniques from alternating tree automata to the realm of
Markov chains. The resulting pautomata determine languages of Markov
chains which are proved to be closed under Boolean operations, to
subsume bisimulation equivalence classes of Markov chains, and to
subsume the set of models of any PCTL formula.
Our acceptance game for an input Markov chain to a pautomata is shown
to be welldefined and to be in EXPTIME in general; but its complexity
is that of PCTL model checking for automata that represent PCTL
formulas. We also derive a notion of simulation between pautomata
that approximates language containment in EXPTIME.
These foundations therefore enable abstractionbased probabilistic
model checking for probabilistic specifications that subsume Markov chains, and
LTL and CTL* like logics.

12:30 PM  Lunch

02:00 PM  Catuscia Palamidessi
 InformationTheoretic Approaches to Information Flow and Model Checking Techniques to Measure it [slides  video]
In recent years, there has been a growing interest in considering the quantitative aspects of
Information Flow, partly because often the a priori knowledge of the secret information can be
represented by a probability distribution, and partly because the mechanisms to protect the
information may use randomization to obfuscate the relation between the secrets and the
observables. Among the quantitative approaches to Information Flow, the most prominent is
the one based on Information Theory, which interprets a system producing information leakage as
a (noisy) channel between the secrets (input) and the observables (output), and the leakage itself
as the difference between the Shannon entropies of the input before and after the output (Mutual
Information). This approach however suffers from two shortcomings:
(1) The Shannon entropy is not the most suitable measure in case of the typical attacks in
security (in particular, the onetry attacks), and
(2) the analogy with the (simple) channel collapses in case of an interactive system.
In this talk we discuss these issues and propose some solutions. Finally, we discuss some
methods, based on model checking, to compute the Information Flow associated to a system.

02:30 PM  Rajeev Alur
 Architectureaware Analysis of Concurrent Software [slides  video]
Our ability to effectively harness the computational power of multiprocessor
and multicore architectures is predicated upon advances in programming
languages and tools for developing concurrent software. Recent years have seen
intensive research in methods for verifying concurrent software resulting in
powerful tools for finding concurrencyrelated bugs. Almost all of such tools
are based on the assumption that the instructions of the same thread are
executed according to the program order. This model is called the interleaving
model in the verification community, and the sequential consistency model
in the computer architecture literature. While this is a commonly accepted
languagelevel memory model, modern multiprocessors relax sequential
consistency in different ways for performance reasons resulting in weaker
models. The goal of our research is to develop tools for analyzing systemlevel
concurrent software along with such details of the underlying architecture. A
first step in our research has resulted in a tool called CheckFence. CheckFence
analyzes C code for concurrent data types with respect to an axiomatic
specification of a memory model. Using a satisfiability solver, for a given
client test program, CheckFence searches for discrepancy between operationlevel
sequential consistency semantics for the data type and concurrent executions
feasible with respect to the specified model. We have analyzed a number of
benchmarks successfully using CheckFence. Our analysis has revealed a number of
potential bugs, and the memory ordering fences needed to fix the bugs. We
conclude by discussing research opportunities and challenges for analysis tools
that can bridge the gap between the programmers' desire for simplicity of
concurrency abstractions and architects' ability to expose hardware parallelism.

03:00 PM  WillemPaul De Roever
 What is in a Step: New Perspectives on a Classical Question
[slides:
1
2
3  video]
In their seminal 1991 paper "What is in a Step: On the Semantics of
Statecharts", Pnueli and Shalev showed how, in the presence of global
consistency and while observing causality, the synchronous language
Statecharts can be given coinciding operational and declarative
macrostep semantics. Over the past decade, this semantics has been
supplemented with denotational, gametheoretic and axiomatic
characterisations, thus revealing itself as a rather canonical
interpretation of the synchrony hypothesis. In this paper, we survey
these characterisations and use them to emphasise the close but not
widely known relations of Statecharts to the synchronous language
Esterel and to the field of logic programming. Additionally, we
highlight some early reminiscences on Amir Pnueli's first attempts
to characterise the semantics of Statecharts.

03:30 PM  Break

04:00 PM  Muli Safra
 Collaboration with Amir: what are the chances? [slides  video]

04:30 PM  Lenore Zuck
 Amir: The Axis of Acsys [slides  video  video: How Amir Liked Things To Work]

Sponsors
We gratefully acknowledge the support of the following sponsors:
Organizing Committee
Speakers
Rajeev Alur
 University of Pennsylvania
 Philadelphia, Pennsylvania, USA

Krzysztof Apt
 Centrum Wiskunde and Informatica
 Amsterdam, Netherlands

Egon Börger
 Università di Pisa
 Pisa, Italy

Manfred Broy
 Technische Universität München  München, Germany

Patrick Cousot
 New York University
 New York, New York, USA

Werner Damm
 Carl von Ossietzky Universität Oldenburg
 Oldenburg, Germany

WillemPaul De Roever
 ChristianAlbrechtsUniversität zu Kiel
 Kiel, Germany

Allen Emerson
 The University of Texas at Austin
 Austin, Texas, USA

Javier Esparza
 Technische Universität München
 München, Germany

David Harel
 The Weizmann Institute of Science
 Rehovot, Israel

Tom Henzinger
 EPFL
 Lausanne, Switzerland

Robert Kurshan
 Cadence Design Systems
 New York, New York, USA

Leslie Lamport
 Microsoft Research
 Mountain View, CA, USA

Oded Maler
 CNRSVerimag
 Grenoble, France

Ken McMillan
 Cadence Research Labs
 Berkeley, CA, USA

Stephan Merz
 INRIA Lorraine, LORIA
 Nancy, France, USA

Catuscia Palamidessi  École Polytechnique
 Palaiseau, France

Krishna Palem
 Rice University
 Houston, Texas, USA

Nir Piterman
 Imperial College London
 London, UK

Roni Rosner
 Intel  Israel Design Center
 Haifa, Israel

Muli Safra
 Tel Aviv University
 Tel Aviv, Israel

Giora Slutzki
 Iowa State University
 Ames, Iowa, USA

Ofer Strichman
 Technion
 Haifa, Israel

P.S. Thiagarajan
 National University of Singapore
 Singapore

Moshe Vardi
 Rice University
 Houston, Texas, USA

Lenore Zuck
 University of Illinois at Chicago
 Chicago, Illinois, USA

top  contact webmaster@cs.nyu.edu
