Fabio Mogavero

Parity games are two-player infinite-duration games on numerically labeled
graphs, playing a crucial role in various fields of theoretical computer
science. Finding efficient algorithms to solve these games in practice is widely
acknowledged as a core problem in formal verification, as it leads, indeed, to
efficient solutions of the model-checking and satisfiability problems for
expressive temporal logics, e.g., the modal µCalculus. This problem has also an
intriguing status from a complexity theoretic viewpoint, since it belongs to the
class UPTime ∩ CoUPTime, and still open is the question whether it can be solved
in polynomial time. The solution of a parity game can be reduced to the problem
of identifying sets of positions of the game, called dominions, in each of which
a player can force a win by remaining in the set forever. In this talk, we
describe a novel technique to compute dominions, based on the idea of promoting
positions to higher priorities during the search for winning regions. The
proposed approaches have nice computational properties, exhibiting the best
space complexity among the currently known solutions. Experimental results on
both random games and benchmark families show that the technique is also very
effective in practice.
The talk is based on joint works with Massimo Benerecetti and Daniele Dell’Erba
of the Università degli Studi di Napoli Federico II.

Shaull Almagor

We consider the following problem: given a dxd matrix A and two polytopes P and Q, is there a natural number n such that A^n P intersects Q. We show that the problem can be decided in PSPACE for dimension at most three. As in previous works, decidability in the case of higher dimensions is left open, as the problem is known to be hard for long-standing number-theoretic open problems.

The talk is self-contained and assumes no background from the audience. As such, the talk will include short introductions to various mathematical tools, such as representation of algebraic numbers, the theory of real-closed fields, and quantifier elimination.

Malte Schwarzkopf

Scheduling tasks on clusters in large-scale datacenters is challenging:
thousands of tasks must be cleverly and quickly placed to achieve good
application-level performance and high resource utilization. Centralized
datacenter schedulers can make high-quality placement decisions, but
today these high-quality placements come at the cost of high latency at
scale, which degrades response time for interactive tasks and reduces
resource utilization.

In this talk I present Firmament, a centralized scheduler that scales to
over ten thousand machines, even though it performs a computationally
expensive min-cost max-flow (MCMF) optimization that continuously
reschedules all tasks. To achieve this, Firmament automatically chooses
between different MCMF algorithms, solves the optimization problem
incrementally when possible, and applies problem-specific optimizations.

Experiments with a Google workload trace from a 12,500-machine cluster
show that Firmament places tasks in hundreds of milliseconds, and that
Firmament improves placement latency by 20x over Quincy, a prior
centralized scheduler using the same MCMF optimization. Moreover, even
though Firmament is centralized, it matches the placement latency of
distributed schedulers for workloads of short tasks. Finally, Firmament
exceeds the placement quality of four widely-used centralized and
distributed schedulers on a real-world cluster, improving batch task
response time by 6x.

I. Gog, M. Schwarzkopf, A. Gleave, R. N. M. Watson, S. Hand. “Firmament:
Fast, Centralized Cluster Scheduling at Scale”. In Proceedings of the
12th USENIX Symposium on Operating Systems Design and Implementation
(OSDI), Savannah, GA, USA, November 2016, p. 99–115.

Rupak Majumdar

[Software Testing] Hitting families of schedules

We consider the following basic task in the testing of concurrent systems.
The input to the task is a partial order of events, which models actions performed on or by the system and specifies ordering constraints between them. The task is to determine if some scheduling of these events can result in a bug. The number of schedules to be explored can, in general, be exponential.

Empirically, many bugs in concurrent programs have been observed to have small bug depth; that is, these bugs are exposed by every schedule that orders some d specific events in a particular way, irrespective of how the other events are ordered, and d is small compared to the total number of events. To find all bugs of depth $d$, one needs to only test a d-hitting family of schedules: we call a set of schedules a $d$-hitting family if for each set of d events, and for each allowed ordering of these events, there is some schedule in the family that executes these
events in this ordering. The size of a d-hitting family may be much smaller than the number of all possible schedules, and a natural question is whether one can find $d$-hitting families of schedules that have small size.

In general, finding the size of optimal d-hitting families is hard, even for d=2. We show, however, that when the partial order is a tree, one can explicitly construct d-hitting families of schedules of small size. When the tree is balanced, our constructions are polylogarithmic in the number of events.

Dirk Beyer

Correctness Witnesses: Exchanging Verification Results between Verifiers
Dirk Beyer

Paper: http://dx.doi.org/10.1145/2950290.2950351
Proc. SIGSOFT FSE 2016.

Standard verification tools provide a counterexample to witness a specification violation,
and, since a few years, such a witness can be validated by an independent validator
using an exchangeable witness format. This way, information about the violation can be shared across verification tools and the user can use standard tools to visualize and explore witnesses.
This technique is not yet established for the correctness case, where a program fulfills a specification. Even for simple programs, it is often difficult for users to comprehend why a given program is correct, and there is no way to independently check the verification result.
We close this gap by complementing our earlier work on violation witnesses with correctness witnesses. While we use an extension of the established common exchange format for violation witnesses to represent correctness witnesses, the techniques for producing and validating correctness witnesses are different. The overall goal to make proofs available to engineers is probably as old as programming itself, and proof-carrying code was proposed two decades ago —
our goal is to make it practical: We consider witnesses as first-class exchangeable objects, stored independently from the source code and checked independently from the verifier that produced them, respecting the important principle of separation of concerns.
At any time, the invariants from the correctness witness can be used to reconstruct a correctness proof to establish trust. We extended two state-of-the-art verifiers, CPAchecker and Ultimate Automizer, to produce and validate witnesses, and report that the approach is promising
on a large set of verification tasks.

Jan Strejček

Partial but Precise Loop Summarization and Its Applications

We show a symbolic-execution-based algorithm computing the precise effect of a program cycle on
program variables. For a program variable, the algorithm produces an expression representing
the variable value after the number of cycle iterations specified by parameters of the
expression. The algorithm is partial in the sense that it can fail to find such an expression
for some program variables (for example, it fails in cases when the variable value depends on
the order of paths in the cycle taken during iterations).

We present two applications of this loop summarization procedure. The first is a construction
of a nontrivial necessary condition on program input to reach a given program location. The
second application is a loop bound detection algorithm, which produces tighter loop bounds than
other approaches.

Pavol Cerny

Software-defined networking (SDN) programs must simultaneously
describe static forwarding behavior and dynamic updates in response to
events. Event-driven updates are critical to get right, but
difficult to implement correctly due to the high degree of concurrency
in networks. Existing SDN platforms offer weak guarantees that can
break application invariants, leading to problems such as dropped
packets, degraded performance, and security violations. We
introduce event-driven consistent updates that are
guaranteed to preserve well-defined behaviors when transitioning
between configurations in response to events. We propose network
event structures (NESs) to model constraints on updates, such as
which events can be enabled simultaneously and causal dependencies
between events. We define an extension of the NetKAT language with
mutable state, give semantics to stateful programs using NESs, and
discuss strategies for implementing NESs in SDNs.
Finally, we evaluate our approach empirically,
demonstrating that it gives well-defined consistency guarantees while
avoiding expensive synchronization and packet buffering.

This is joint work with Jedidiah McClurg, Hossein Hojjat, and Nate Foster.

Martin Schäf

We present an approach to the classification of error messages in the context of static checking in the style of ESC/Java. The idea is to compute a semantics-based signature for each error message and then group together error messages with the same signature. The approach aims at exploiting modern verification techniques based on, e.g., Craig interpolation in order to generate small but significant signatures. We have implemented the approach and applied it to three benchmark sets (from Apache Ant, Apache Cassandra, and our own tool). Our experiments indicate an interesting practical potential. More than half of the considered error messages (for procedures with more than just one error message) can be grouped together with another error message.

Martin Schäf is a Computer Scientist at SRI International. Before joining SRI, he worked at the United Nations University in Macau. He received his PhD from University of Freiburg in 2011, and his MS degree in computer science from Saarland University in 2006. His research interests include static analysis, software verification, fault localization, and GUI testing.

Branislav Bošanský

We study dynamic games with finite horizon. These games evolve in time and the players are able to observe and react to information during the course of the game. We assume the players have imperfect information and there can be stochastic events. The problem of finding optimal strategies is determined in many subclasses of finite dynamic games and for many game-theoretic solution concepts – including maxmin strategies or a Stackelberg equilibrium, where one player publicly commits to a strategy, to which the second player plays a best response. During the talk I will describe some of the algorithmic challenges when computing maxmin and Stackelberg strategies and our recent domain-independent algorithms that overcome these challenges.

João Sousa Pinto

We consider a continuous analogue of Babai et al.’s and Cai et al.’s problem of solving multiplicative matrix equations. Given k+1 square matrices A_1, …, A_k, C, all of the same dimension, whose entries are real algebraic, we examine the problem of deciding whether there exist non-negative reals t_1, …, t_k such that exp(A_1 t_1)…exp(A_kt_k) = C.
We show that this problem is undecidable in general, but decidable under the assumption that the matrices A_1,…,A_k commute. Our results have applications to reachability problems for linear hybrid automata. Our decidability proof relies on a number of theorems from algebraic and transcendental number theory, most notably those of Baker, Kronecker, Lindemann, and Masser, as well as some useful geometric and linear-algebraic results, including the Minkowski-Weyl theorem and a new (to the best of our knowledge) result about the uniqueness of strictly upper triangular matrix logarithms of upper unitriangular matrices. On the other hand, our undecidability result is shown by reduction from Hilbert’s Tenth Problem.