Reachability analysis is a useful tool for checking whether a cyber-physical system satisfies a given safety property. For instance, one could ask whether an electro-magnetic braking system brings a car to a standstill within a given time frame. In set-based reachability, one takes a given set of initial states (ranges for the position and speed of the car) and computes the image of the set of states as it evolves over time. Even for simple types of systems, this so-called reach set can only be computed approximately, and accuracy comes at an extremely steep cost. A highly scalable way to approximate the reach set is known for the special case of linear dynamics. It is based on template polyhedra, which are polyhedra (sets bounded by linear constraints) with normal vectors from a given finite set. Simple instances of template polyhedra are boxes or octagons. A template instance that tightly bounds the reach set is found by solving a set of optimization problems. The accuracy of the approximation can be improved by adding more normal vectors to the template.

In this talk, we propose an approach that extends this idea from linear to nonlinear dynamics. We linearize the system around a reference trajectory and solve ODEs to obtain templates that bound the reach set. The ODEs are particular in that they involve an optimization problem constrained by the template itself. We show how, similarly to the linear case, the template can be adapted over time to match the dynamics of the system. For both static and dynamic templates, we identify conditions that guarantee convergence. The potential of the approach is discussed on several benchmarks.

Asynchronous concurrency is a model of concurrency based on the concept of tasks. It executes tasks one-at-a-time, choosing the next task to run from a set called the task buffer, adding tasks to the buffer using a “post” primitive, and scheduling a new task only when the currently running task gives up control. Task can depend on each other using explicit “wait” operations. This model and its variants are used widely in languages such as JavaScript, C# (the async and await primitives), or the monadic concurrency libraries of Haskell and OCaml. The more restricted scheduling separates it from the more commonly considered multi-threaded programming model.

In this talk, I will address talk about two projects. The first project deals with the question how we can reason about asynchronous programs. We present a program logic and a corresponding type system that allow us to reason locally about programs with asynchronous concurrency and mutable state; we instantiate this model for OCaml using the Lwt library. The key innovation is to introduce the concept of a “wait permission”, which describes the resources that a given task will yield on termination. An earlier version of this work was published at ECOOP ’15. The second project deals with the question how we can perform a kind of “asynchronous parallelization” optimization, where we are given a (more-or-less) sequential program and rewrite it to make use of asynchronous concurrency. We use a set of program rewriting rules, most notably replacing synchronous I/O operations with asynchronous counterparts in a safe way, and pushing wait statements as far back as possible. As it turns out, proving the soundness of these rewriting rules is surprisingly tricky; I will sketch a reasoning approach that allows us to show refinement, in the the following sense: Let $e$ be a program, and $e’$ the result of rewriting $e$ using the given rules. For every terminating execution of $e’$, there is a corresponding terminating execution of $e$ that ends in an equivalent state.

The central problem addressed in this talk is the following: given the design of a hybrid system, conclude if the system is stable. Hybrid systems are apt to model cyber-physical systems since they capture the mixed discrete-continuous behaviour which appears naturally in cyber-physical systems. Stability is a fundamental property in control system design, which demands that small perturbations in the input to the system lead to small variations in the future behaviour. The classical approach to establishing stability involves finding a particular kind of function, called Lyapunov function. In relation to this method, there is some effort towards automation which consists of a template-based search that uses sum-of-squares solvers. However, the shortcomings with this template-based method are that the choice of a correct template requires designer’s ingenuity and that a template failure does not provide instability reasons or guidance for the choice of the next template.

We propose an alternate algorithmic approach for the stability verification of hybrid systems, which is a counterexample-guided abstraction refinement (CEGAR) framework. The key idea is that given a hybrid system, its stability can be determined by constructing an abstract weighted graph which over-approximates the behaviour of the former one. The relation between the abstraction and the hybrid system is such that if every cycle in the graph has weight below 1, then the hybrid system is stable. In the case that the graph has a cycle with weight greater than 1, this cycle can be evaluated to infer instability of the hybrid system or guide the choice of subsequent templates. This CEGAR approach addresses the shortcomings of the template-based search.

We have implemented the CEGAR algorithm in the tool AVERIST, and we report experimental evaluations on some examples for demonstrating the feasibility of the approach.

In this talk I will discuss a new generation of software tools based on probabilistic models learned from large codebases of code a.k.a “Big Code”. By leveraging the massive effort already spent by thousands of programmers, these tools make useful predictions about new, unseen programs, thus helping to solve important and difficult software tasks. As an example, I will illustrate our systems for statistical code completion, deobfuscation and defect prediction. Two of these systems (jsnice.org and apk-deguard.com) are freely available and already have thousands of users. In the talk, I will present some of the core machine learning and program analysis techniques behind these learning tools.

Short Bio: Veselin Raychev obtained his PhD from ETH Zürich in 2016 and his dissertation “Learning from Large Codebases” has received Honorable Mention for 2016 ACM Doctoral Dissertation Award. Before his PhD, he worked as a software engineer at Google on the public transportation routing algorithm of Google Maps as well as several other projects. Currently he is a co-founder and CTO of DeepCode GmbH – a company developing “Big Code” programming tools.

The talk will have three parts in which I will discuss the results achieved with my colleagues about nondeterministic, deterministic, and semi-deterministic omega-automata. For nondeterministic automata, I will show which aspects of property automata can influence the performance of explicit model checking and what improvements can be made in LTL-to-automata traslation if we have some knowledge about the verified system. Then I will present our efficient translation of a fragment of LTL to deterministic automata. Finally, I will explore the jungle of Buchi automata classes that lie between deterministic and nondeterministic automata. I will present how to efficiently complement semi-deterministic automata and how to obtain them from nondeterministic generalized Buchi automata.

Every day, we make sequences of decisions to accomplish our goals, and we attempt to achieve these goals in the most favorable way. In many aspects of life, such as in security or economy, the optimality of these decisions is critical, and a computational support for decision making is thus needed. Sequential decision making is, however, computationally challenging in the presence of uncertainty (partially observable Markov decision processes) or even adversaries (partially observable stochastic games). We provide a game theoretic model of one-sided partially observable stochastic games which is motivated by problems arising mainly in security. It captures both the uncertainty of the decision maker and the adversarial nature of the problem into account. Our framework assumes two players where one player is given the advantage of having perfect information. We show that we can solve such games in the similar fashion as one solves POMDPs using the value iteration algorithm, including its more practical approximate variants based on point-based updates of the value function.

Languages K and L are separable by language S if K is included in S and L is disjoint from S.

I will present recent results on decidability of the problem whether two languages of one counter automata are separable

by some regular language.

Virtually all real-valued computations are carried out using floating-point data types and operations. With the current emphasis of system development often being on computational efficiency, developers as well as compilers are increasingly attempting to optimize floating-point routines. Reasoning about the correctness of these optimizations is complicated, and requires error analysis procedures with different characteristics and trade-offs. In my talk, I will motivate the need for such analyses. Then, I will present both a dynamic and a rigorous static analysis we developed for estimating errors of floating-point routines. Finally, I will describe how we extended our rigorous static analysis into a procedure for mixed-precision tuning of floating-point routines.

Short bio:

Zvonimir Rakamaric is an assistant professor in the School of Computing at the University of Utah. Prior to this, he was a postdoctoral fellow at Carnegie Mellon University in Silicon Valley, where he worked closely with researchers from the Robust Software Engineering Group at NASA Ames Research Center to improve the coverage of testing of NASA’s flight critical systems. Zvonimir received his bachelor’s degree in Computer Science from the University of Zagreb, Croatia; he obtained his M.Sc. and Ph.D. from the Department of Computer Science at the University of British Columbia, Canada.

Zvonimir‘s research mission is to improve the reliability and resilience of complex software systems by empowering developers with practical tools and techniques for analysis of their artifacts. He is a recipient of the NSF CAREER Award 2016, Microsoft Research Software Engineering Innovation Foundation (SEIF) Award 2012, Microsoft Research Graduate Fellowship 2008-2010, Silver Medal in the ACM Student Research Competition at the 32nd International Conference on Software Engineering (ICSE) 2010, and the Outstanding Student Paper Award at the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2007.

For more information about Zvonimir, visit www.zvonimir.info.