Games for Formal Design and Analysis of Reactive Systems
Rajeev Alur, University of Pennsylvania,
With recent advances in algorithms for state-space traversal and in techniques for automatic
abstraction of source code, model checking has emerged as a key tool for analyzing and debugging
software systems. This talk discusses the role of games in modeling and analysis of software systems.
Games are useful in modeling open systems where the distinction among the choices controlled by
different components is made explicit. We first describe the model checker Mocha that supports
a game-based temporal logic for writing requirements, and its applications to analysis of multi-party
security protocols. Then, we describe how to automatically extract dynamic interfaces for Java classes
using predicate abstraction for extracting a boolean model from a class file, and learning
algorithms for constructing the most general strategy for invoking the methods of the model. We discuss
an implementation in the tool JIST---Java Interface Synthesis Tool, and demonstrate that
the tool can construct interfaces, accurately and efficiently, for sample Java2SDK library classes.
We will conclude with a discussion of how game-based analysis can be used to synthesize systems
from their specifications.
Constraint based synthesis from sketches to storyboards and beyond
Synthesis approaches based on constraint solving offer some unique opportunities to experiment with more natural and more interactive forms of collaboration between programmers and synthesis engines. This talk will describe how constraint based synthesis technology can enable a multi-modal programming model, where programmers can combine insights in different forms ranging from low-level insights about the structure of the desired program to high-level graphical intuitions about how the program modifies its state. The talk will elaborate on some of the technical challenges involved in making new forms of interaction possible, as well as some of the open problems behind this technology.
We consider the problem of specifying combinations of concurrent data
structures with complex sharing in a manner that is both declarative
and results in provably correct code. In our approach, abstract
concurrent data types are specified using relational algebra and
functional dependencies. We describe (1) a language of decompositions that
permit the user to specify different combinations of data
structures to represent a relation, and (2) a language of lock placements
that allow the user to specify a range of conservative and speculative
locking strategies at a variety of granularities. We show that given a
decomposition and a lock placement, a compiler can generate
serializable transactions that operate over decomposed relations.
Finally we describe an autotuner that can simultaneously explore the
space of decompositions and lock placements to synthesize an optimal
combination of data structures and locks.
We argue for a programming model where automated reasoning plays a key
role during (1) interactive program development, (2) program
compilation, and (3) program execution. I will focus on data
manipulation (as opposed to control). I outline our results in
complete functional synthesis for integer arithmetic, which is a form
of program compilation based on decision procedures. For program
development, I sketch our ongoing work on resolution theorem proving
for interactive synthesis. For program execution, I touch upon the
UDITA system based on Java Pathfinder, and argue that programming
models related to constraint logic programming should play a bigger
role in mainstream software.
For more information, please see: http://lara.epfl.ch/w/impro