Wednesday, February 25
- Moshe Vardi (Houston): The Rise and fall of Linear Temporal Logic
- Bernd Finkbeiner (Saarbrücken): Distributed Synthesis
One of the surprising developments in the area of program verification in the late part of the 20th Century is the emergence of Linear Temporal Logic (LTL), a logic that emerged in philisophical studies of free will, as the canonical language for describing temporal behavior of computer systems. LTL, however, is not expressive enough for industrial applications. The first decade of the 21 Century saw the emergence of industrial temporal logics such as ForSpec, PSL, and SVA. These logics, however, are not clean enough to serve as objects of theoretical study. This talk will describe the rise and fall of LTL, and will propose a new canonical temporal logic: Linear Dynamic Logic (LDL).
More than fifty years after its introduction by Alonzo Church, the synthesis problem is still one of the most intriguing challenges in the theory of reactive systems. On the one hand, synthesis algorithms have found applications in many areas of computer science and systems engineering, from the construction and optimization of circuits and device drivers to the synthesis of controllers for robots and manufacturing plants. On the other hand, the logical and algorithmic foundations of the synthesis problem are still far from complete. In this talk, I will focus on the problem of synthesizing distributed systems, a particularly interesting, and also particularly difficult, version of the synthesis problem. I will give an overview of the state of the art in models, logics, and algorithms for the synthesis of distributed systems and present ideas for future directions.
Thursday, February 26
- Jean-Francois Raskin (Brussels): Variations on the stochastic shortest path problem
- Azadeh Farzan (Toronto): Succinct Proofs of Concurrent Programs
In this talk, we revisit the stochastic shortest path problem, and show how results allow one to improve over the classical solutions: we present algorithms to synthesize strategies with multiple guarantees on the distribution of the length of paths reaching a given target, rather than simply minimizing its expected value. The concepts and algorithms that we propose here are applications of more general results that have been obtained recently for Markov decision processes and that are described in a series of recent papers.
In this talk, I will briefly look at the general trends in the history of proof methods for concurrent programs, and the dominant quest for compositional proof methods. I will then talk about the recent progress that my colleagues and I have made in this area. The key observation is that compositionality is not the only way of achieving succinctness in proofs, and decidability or tractability in the verification process.
Friday, February 27
- Eric Bodden (Darmstadt): SPLlift: statically analyzing software product lines in minutes instead of years
- Joel Ouaknine (Oxford): Termination of Linear Loops: Algorithmic Advances and Challenges
A software product line (SPL) encodes a potentially large variety of software products as variants of some common code base. Up until now, re-using traditional static analyses for SPLs was virtually intractable, as it required programmers to generate and analyze all products individually. In this talk, however, I will show how an important class of existing inter-procedural static analyses can be transparently lifted to SPLs. Without requiring programmers to change a single line of code, our approach SPLlift automatically converts any analysis formulated for traditional programs within the popular IFDS framework for inter-procedural, finite, distributive, subset problems to an SPL-aware analysis formulated in the IDE framework, a well-known extension to IFDS. Using a full implementation based on Heros, Soot, CIDE and JavaBDD, we were able to show that with SPLlift one can reuse IFDS-based analyses without changing a single line of code. Experiments using three static analyses applied to four Java-based product lines showed that the approach produces correct results and outperforms the traditional approach by several orders of magnitude.
In the quest for program analysis and verification, program termination -- determining whether a given program will always halt or could execute forever -- has emerged as a pivotal component. Unfortunately, this task was proven to be undecidable by Alan Turing eight decades ago, before the advent of the first working computers! In recent years, however, great strides have been made in the automated analysis of termination of programs, from simple counter machines to Windows device drivers.
In this talk, I will focus, from a theoretical (i.e. decidability and complexity) point of view, on the special case of simple linear loops, i.e., un-nested WHILE programs with linear assignments and linear exit conditions (and no conditionals, side effects, nothing). Somewhat surprisingly, the study of termination of simple linear loops involves advanced techniques from a variety of mathematical fields, including analytic and algebraic number theory, Diophantine geometry, and real algebraic geometry. I will present an overview of known results, and discuss existing algorithmic challenges and open problems.
This is joint work with James Worrell.