Select program by conference(s):


Select program by day:

Monday 3.Sept. Tuesday 4.Sept. Wednesday 5.Sept Thursday 6.Sept

Tuesday, 4. September

Registration [Location: 2nd floor, Hörsaalzentrum]

The registration desk will be opened from 8:30 a.m. It is located in the second floor of the building while the conference rooms (lecture halls HZ 10 and HZ 11) are in the third floor of the building.
Today, the registration desk closes at 14:45 to prepare the social event.

PPDP & LOPSTR: Joint Invited Talk [Chair: Peter Thiemann  • Location: HZ 10 (third floor, Hörsaalzentrum)]
Formal methods for JavaScript (Invited Talk)
Philippa Gardner

We present a novel, unified approach to the development of compositional symbolic execution tools, which bridges the gap between traditional symbolic execution and compositional program reasoning based on separation logic. We apply our approach to JavaScript, providing support for full verification, whole-program symbolic testing, and automatic compositional testing based on bi-abduction.

Coffee Break [Location: 2nd floor, Hörsaalzentrum]
PPDP: Contributed Talks #4 [Chair: Annette Bienusa • Location: HZ 10 (third floor, Hörsaalzentrum)]
Certified Compilation of Financial Contracts
Danil Annenkov and Martin Elsman

We present an extension to a certified financial contract management system that allows for templated declarative financial contracts and for integration with financial stochastic models through verified compilation into so-called payoff expressions. Such expressions readily allow for determining the value of a contract in a given evaluation context, such as contexts created for stochastic simulations. The templating mechanism is useful both at the contract specification level, for writing generic reusable contracts, and for reuse of code that, without the templating mechanism, needs to be recompiled for different evaluation contexts. We report on the effect of using the certified system in the context of a GPGPU-based Monte Carlo simulation engine for pricing various over-the-counter (OTC) financial contracts. The full contract-management system, including the payoff-language compilation, is verified in the Coq proof assistant and certified Haskell code is extracted from our Coq development along with Futhark code for use in a data-parallel pricing engine.

Two-Phase Dynamic Analysis of Message-Passing Go Programs based on Vector Clocks
Martin Sulzmann and Kai Stadtmüller

Understanding the run-time behavior of concurrent programs is a challenging task. A popular approach is to establish a happens-before relation via vector clocks. Thus, we can identify bugs and performance bottlenecks, for example, by checking if two conflicting events may happen concurrently. We employ a two-phase method to derive vector clock information for a wide range of concurrency features that includes all of the message-passing features in Go. The first instrumentation phase yields a run-time trace that contains all events that took place. The second trace replay phase carried out offline infers vector clock information. Trace replay operates on thread-local traces. Thus, we can observe behavior that might result from some alternative schedule. Our approach is not tied to any specific language. We have built a prototype for the Go programming language and provide empirical evidence of the usefulness of our method.

Transformation of Combinatorial Optimization Problems Written in Extended SQL into Constraint Problems
Genki Sakanashi and Masahiko Sakai

The combinatorial optimization is an important area, which gives one of the best solutions for our real problems. This paper focuses on an SQL style of declarative languages to ease descriptions of combinatorial optimization problems, and provides their solution method powered by state-of-the-art CP/SMT solvers. From the semantic point of view, the search space of a combinatorial problem is given as a finite set of relations, and a solution is a relation in the set. Relations in the search space are filtered by constraints of the problem in similar to the filter-function on lists in functional languages, and the remaining relations are solutions of the problem. According to this notion, we extended Structured Query Language (SQL) by introducing some operations on sets of relations: generating a set of relations, filtering a set of relations according to constraints, and selecting one of the optimum relations with respect to a goal function. Toward an effective implementation, a set of relations is represented as a pair of a relation containing variables with finite domains and constraints on variables. This enables to solve the target problem by CP/SMT solvers. We also give an experimental result on the graph vertex coloring problem.

LOPSTR: Analysis of TRS [Chair: Vincent Nys • Location: HZ 11 (third floor, Hörsaalzentrum)]
Proving Program Properties as First-Order Satisfiability
Salvador Lucas

Program semantics can often be expressed as a (many-sorted) first-order theory S, and program properties as sentences φ which are intended to hold in the canonical model of such a theory, which is often incomputable. Recently, we have shown that properties φ expressed as the existential closure of a boolean combination of atoms can be disproved by just finding a model of S and the negation ¬φ of φ. Furthermore, this idea works quite well in practice due to the existence of powerful tools for the automatic generation of models for (many-sorted) first-order theo- ries. In this paper we extend our previous results to arbitrary properties, expressed as sentences without any special restriction. Consequently, one can prove a program property φ by just finding a model of an appropri- ate theory (including S and possibly something else) and an appropriate first-order formula related to φ. Beyond its possible theoretical interest, we show that our results can also be of practical use in several respects.

Guided Unfoldings for Finding Loops in Standard Term Rewriting
Étienne Payet

In this paper, we reconsider the unfolding-based technique that we have introduced previously for detecting loops in standard term rewriting. We improve it by guiding the unfolding process, using distin- guished positions in the rewrite rules. This results in a depth-first compu- tation of the unfoldings, whereas the original technique was breadth-first. We have implemented this new approach in our tool NTI and compared it to the previous one on a bunch of rewrite systems. The results we get are promising (better times, more successful proofs).

Homeomorphic Embedding modulo Combinations of Associativity and Commutativity Axioms
María Alpuente, Angel Cuenca-Ortega, Santiago Escobar, and José Meseguer

The Homeomorphic Embedding relation has been amply used for defining termination criteria of symbolic methods for program analysis, transformation, and veri- fication. However, homeomorphic embedding has never been investigated in the context of order-sorted rewrite theories that support symbolic execution methods modulo equa- tional axioms. This paper generalizes the symbolic homeomorphic embedding relation to order–sorted rewrite theories that may contain various combinations of associativity and/or commutativity axioms for different binary operators. We systematically measure the performance of increasingly efficient formulations of the homemomorphic embed- ding relation modulo associativity and commutativity axioms. From our experimental results, we conclude that our most efficient version indeed pays off in practice.

Lunch Break [Location: Mensa Casino]
PPDP: Contributed Talks #5 [Chair: Michael Hanus • Location: HZ 10 (third floor, Hörsaalzentrum)]
Automatic reordering for dataflow safety of Datalog
Mistral Contrastin, Dominic Orchard and Andrew Rice

Automatic Reordering for Dataflow Safety of Datalog Abstract: Clauses and subgoals in a Datalog program can be given in any order without affecting program meaning. However, practical applications of the language require the use of built-in or external predicates with particular dataflow requirements. These can be expressed as input or output modes on arguments. We describe a static analysis of moding for Datalog which can transform an ill-moded program into a well-moded program by reordering clause subgoals, satisfying dataflow requirements. We describe an incremental algorithm which efficiently finds a reordering if it exists. This frees the programmer to focus on the declarative specification of their program rather than on the implementation details of external predicates. We prove that our computed reorderings yield well-moded programs (soundness) and that if a program can be made well-moded, we compute a reordering to do so (completeness).

Improving Refutational Completeness of Relational Search via Divergence Test
Dmitri Rozplokhas and Dmitry Boulytchev

We describe a search optimization technique for implementation of relational programming language miniKanren which makes more queries to converge. Specifically, we address the problem of conjunction non-commutativity. Our technique is based on a certain divergence criterion, which we use to trigger a dynamic reordering of conjuncts. We present a formal semantics of a miniKanren-like language and prove that our optimization does not compromise already converging programs, thus, being a proper improvement. We also present the prototype implementation of the improved search and demonstrate its application for a number of realistic specifications.

Web-based Visualisation for Definite Clause Grammars using Prolog Meta-Interpreters
Falco Nogatz, Jona Kalkus and Dietmar Seipel

Definite Clause Grammars (DCGs) are a convenient way to describe lists in Prolog. They are a common mean to specify grammars for natural language processing and to parse formal languages. Despite its long history, tools dedicated to the development and debugging of DCGs are rare. In this paper, we present an interactive, web-based tool to visualise the execution of a DCG. To collect the required information from SWI-Prolog, we discuss several techniques, including meta-interpreters, trace interceptors, and term expansions.

LOPSTR: Around Logic-Based distributed/concurrent programming [Chair: Salvador Lucas • Location: HZ 11 (third floor, Hörsaalzentrum)]
Multiparty Classical Choreographies
Marco Carbone, Luís Cruz-Filipe, Fabrizio Montesi, and Agata Murawska

We present Multiparty Classical Choreographies (MCC), a language model where global descriptions of communicating systems (choreographies) implement typed multiparty sessions. Typing is achieved by generalising classical linear logic to judgements that explicitly record parallelism by means of hypersequents. Our approach unifies different lines of work on choreographies and processes with multiparty sessions, as well as their connection to linear logic. Thus, results developed in one context are carried over to the others. Key novelties of MCC include support for server invocation in choreographies, as well as logic-driven compilation of choreographies with replicated processes.

Correct-by-construction Process Composition Using Classical Linear Logic Inference
Petros Papapanagiotou and Jacques Fleuriot

The need for rigorous process composition is encountered in many situations pertaining to the development and analysis of complex systems. We discuss the use of Classical Linear Logic (CLL) for correct- by-construction resource-based process composition, with guaranteed deadlock freedom, systematic resource accounting, and concurrent execution. We introduce algorithms to automate the necessary inference steps for binary compositions of processes in parallel, conditionally, and in sequence. We combine decision procedures and heuristics to achieve intuitive and practically useful compositions in an applied setting.

Confluence of CHR revisited: invariants and modulo equivalence
Henning Christiansen and Maja H. Kirkeby

Abstract simulation of one transition system by another is introduced as a means to simulate a potentially infinite class of similar transition sequences within a single transition sequence. This is useful for proving confluence under invariants of a given system, as it may reduce the number of proof cases to consider from infinity to a finite number. The classical confluence results for Constraint Handling Rules (CHR) can be explained in this way, using CHR as a simulation of itself. Using an abstract simulation based on a ground representation, we extend these results to include confluence under invariant and modulo equivalence, which have not been done in a satisfactory way before.

Break (No Coffee)

Use this break to walk from the conference location to the start of the city tour (Old Opera Frankfurt).

  • A guided walk will start at 15:15h from Campus Westend. Here is a Google Map with a route description.
  • An alternative is to use the bus no. 64 in direction "Frankfurt (Main) Baseler Platz ". It departs at 15:25 h from "Bremer Straße" and arrives at 15:30h on "Alte Oper" (Old Opera). Get off the bus on the third stop. In this case the following Google Map may be helpful.
The following schematic map may be helpful to find the start of the guided city walk and the dinner location:

Social Event: Guided two hour city walk through the city centre of Frankfurt. [Location: The tour starts in front of the Old Opera Frankfurt]

This city walk through the old town centre (Römerberg) focuses on various aspects of Frankfurt's colourful history, including its role as electoral site of German kings and host city for the coronation ceremonies of Holy Roman emperors. Frankfurt's role as a free trade city and site of Germany's first national assembly, held right here at St Paul's Church in 1848, is also highlighted. The tour covers an abundance of significant events within the smallest of geographical areas.

Conference Dinner [Location: Vinum Frankfurt]