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 8-9, 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.


May 8
08:15 AMWelcome
08:30 AMDavid Harel Can we Verify an Elephant? [slides | video]
09:00 AMKrzysztof 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 AMKrishna 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 microprocessor-based 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 AMBreak
10:30 AMEgon 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 high-level 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 well-known patterns of object-oriented 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 AMManfred Broy Realizability of System Interface Specifications [slides | video]
11:30 AMOfer Strichman Proving Equivalence between Similar Programs: a Progress Report [slides | video]
12:00 PMGiora Slutzki Inverting Proof Systems for Secrecy under OWA [slides | video]
12:30 PMLunch
02:00 PMRobert Kurshan Verification-Guided 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 main-stream model checking and algorithmic drivers of deductive reasoning: preeminently, automatic proof extraction in the context of SAT solving are prevalent. I will describe how abstraction-based 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 PMWerner 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 stability-preserving 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 pre-characterized components supported by compositional and automatable proofs of hybrid interface specifications.
03:00 PMKen McMillan Invisible Invariants: Underapproximating to Overapproximate [slides | video]
In 2001, Pnueli and his co-workers introduced a method they called "invisible invariants". This technique produces proofs of parameterized or infinite-state 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 finite-state model checking. I'll describe the method in terms of abstract interpretation, and relate it to other infinite-state methods, such as indexed predicate abstraction and shape analysis.
03:30 PMBreak
04:00 PMAllen Emerson Time for Time [slides | video]
04:30 PMLeslie Lamport Temporal Logic: The Lesser of Three Evils [slides | video]
05:00 PMStephan Merz A Mechanized Proof System for TLA+ Specifications [slides | video]
May 9
08:30 AMMoshe 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 industry-standard property-specification 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 AMTom Henzinger Quantitative Modeling and Verification [slides | video]
09:30 AMPatrick Cousot A Scalable Segmented Decision Tree Abstract Domain [video]
10:00 AMBreak
10:30 AMOded Maler Properties and Verification in the Continuous Domain [slides | video]
11:00 AMRoni Rosner The Challenge of Evolutionary Verification [slides | pdf | video]
11:30 AMJavier Esparza Newtonian Program Analysis: Solving Sharir and Pnueli's Equations [slides | video]
12:00 PMNir Piterman p-Automata: New Foundations for Discrete-Time 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 p-automata 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 p-automata is shown to be well-defined 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 p-automata that approximates language containment in EXPTIME. These foundations therefore enable abstraction-based probabilistic model checking for probabilistic specifications that subsume Markov chains, and LTL and CTL* like logics.
12:30 PMLunch
02:00 PMCatuscia Palamidessi Information-Theoretic 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 one-try 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 PMRajeev Alur Architecture-aware Analysis of Concurrent Software [slides | video]
Our ability to effectively harness the computational power of multi-processor and multi-core 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 concurrency-related 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 language-level memory model, modern multi-processors relax sequential consistency in different ways for performance reasons resulting in weaker models. The goal of our research is to develop tools for analyzing system-level 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 operation-level 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 PMWillem-Paul 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 macro-step semantics. Over the past decade, this semantics has been supplemented with denotational, game-theoretic 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 PMBreak
04:00 PMMuli Safra Collaboration with Amir: what are the chances? [slides | video]
04:30 PMLenore Zuck Amir: The Axis of Acsys [slides | video | video: How Amir Liked Things To Work]


We gratefully acknowledge the support of the following sponsors:

Organizing Committee

Clark Barrett (Chair) New York University
Patrick Cousot New York University
Ben Goldberg New York University
Radu Grosu SUNY Stony Brook
David Harel The Weizmann Institute of Science
Robert Kurshan Cadence Design Systems
Scott Smolka SUNY Stony Brook
Lenore Zuck University of Illinois at Chicago


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
Willem-Paul De Roever Christian-Albrechts-Universitä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 CNRS-Verimag 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