next day
all days

View: session overviewtalk overviewside by side with other conferences

08:55-10:15 Session 160A: Introduction & Invited Talk 1
Location: FH, Seminarraum 101B
Automating Deductive Synthesis with Leon (Invited Talk)
SPEAKER: Viktor Kuncak
10:15-10:45Coffee Break
10:45-12:45 Session 166E: Contributed Talks 1
Location: FH, Seminarraum 101B
Synthesis of a simple self stabilizing system
SPEAKER: unknown

ABSTRACT. With the increasing importance of distributed systems as a computing paradigm, a systematic approach to the design of distributed systems is needed. Although the area of formal verification has made enormous advances towards this goal, the resulting functionalities are limited to detecting problems in a particular design. We propose a simple template-based approach to computer-aided design of distributed synthesis based on leveraging the well-known technique of bounded model checking to the synthesis setting.

Program Synthesis and Linear Operator Semantics

ABSTRACT. For deterministic and probabilistic programs we investigate the problem of program synthesis and program optimisation (with respect to non-functional properties) in the general setting of global optimisation. This approach is based on the representation of the semantics of programs and program fragments in terms of linear operators, i.e. as matrices. We exploit in particular the fact that we can automatically generate the representation of the semantics of elementary blocks. These can then can be used in order to compositionally assemble the semantics of a whole program, i.e. the generator of the corresponding Discrete Time Markov Chain (DTMC). We also utilise a generalised version of Abstract Interpretation suitable for this linear algebraic or functional analytical framework in order to formulate semantical constraints (invariants) and optimisation objectives (for example performance requirements)

How to Handle Assumptions in Synthesis
SPEAKER: unknown

ABSTRACT. The increased interest in reactive synthesis over the last decade has led to many improved solutions but also to many new questions. In this paper, we discuss the question of how to deal with assumptions on environment behavior. We present four goals that we think should be met and review several different possibilities that have been proposed. We argue that each of them falls short in at least one aspect.

Symblicit algorithms for optimal strategy synthesis in monotonic Markov decision processes
SPEAKER: Aaron Bohy

ABSTRACT. When treating Markov decision processes (MDPs) with large state spaces, using explicit representations quickly becomes unfeasible. Lately, Wimmer et al. have proposed a so-called symblicit algorithm for the synthesis of optimal strategies in MDPs, in the quantitative setting of expected mean-payoff. This algorithm, based on the strategy iteration algorithm of Howard and Veinott, efficiently combines symbolic and explicit data structures, and uses binary decision diagrams as symbolic representation. The aim of this paper is to show that the new data structure of pseudo-antichains (an extension of antichains) provides another interesting alternative, especially for the class of monotonic MDPs. We design efficient pseudo-antichain based symblicit algorithms (with open source implementations) for two quantitative settings: the expected mean-payoff and the stochastic shortest path. For two practical applications coming from automated planning and LTL synthesis, we report promising experimental results w.r.t. both the run time and the memory consumption.

13:00-14:30Lunch Break
14:45-16:00 Session 173B: Invited Talk 2
Location: FH, Seminarraum 101B
Synthesis using EF-SMT Solvers (Invited Talk)
SPEAKER: Ashish Tiwari

ABSTRACT. Satisfiability modulo theory (SMT) solvers check satisfiability of Boolean combination of formulas that contain symbols from several different theories. All variables are (implicitly) existentially quantified. Exists-forall satisfiability modulo theory (EF-SMT) solvers check satisfiability of formulas that have a exists-forall quantifier prefix.  Just as SMT solvers are used as backend engines for verification tools (such as, infinite bounded model checkers and k-induction provers), EF-SMT solvers are potential backends for synthesis tools.  This talk will describe the EF-extension of the Yices SMT solver and present results on using it for reverse engineering hardware. 

16:00-16:30Coffee Break
16:30-18:00 Session 175E: Special Session on Competitions: SyGuS & SyntComp
Location: FH, Seminarraum 101B
The 1st Syntax-Guided Synthesis Competition (SyGuS)
SPEAKER: Rajeev Alur
The 1st Synthesis Competition for Reactive Systems (SyntComp)
SPEAKER: Swen Jacobs