ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Mon 8 Apr 2019 15:00 - 15:30 at SUN I - Verification and Analysis Chair(s): Dirk Beyer

Coupled similarity is a notion of equivalence for systems with internal actions. It has outstanding applications in contexts where internal choices must transparently be distributed in time or space, for example, in process calculi encodings or in action refinements. No tractable algorithms for the computation of coupled similarity have been proposed up to now. Accordingly, there has not been any tool support. We present a game-theoretic algorithm to compute coupled similarity, running in cubic time and space with respect to the number of states in the input transition system. We show that one cannot hope for much better because deciding the coupled simulation preorder is at least as hard as deciding the weak simulation preorder. Our results are backed by an Isabelle/HOL formalization, as well as by a parallelized implementation using the Apache Flink framework.

Mon 8 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 16:00
Verification and AnalysisTACAS at SUN I
Chair(s): Dirk Beyer LMU Munich
14:00
30m
Talk
LCV: A Verification Tool for Linear Controller Software
TACAS
Junkil Park University of Pennsylvania, Miroslav Pajic Duke University, Oleg Sokolsky University of Pennsylvania, USA, Insup Lee
Link to publication
14:30
30m
Talk
Semantic Fault Localization and Suspiciousness Ranking
TACAS
Maria Christakis MPI-SWS, Matthias Heizmann University of Freiburg, Muhammad Numair Mansur Max Planck Institute for Software Systems (MPI-SWS), Christian Schilling IST Austria, Valentin Wüstholz ConsenSys Diligence
Link to publication
15:00
30m
Talk
Computing Coupled Similarity
TACAS
Benjamin Bisping Technische Universität Berlin, Uwe Nestmann
Link to publication
15:30
30m
Talk
Reachability Analysis for Termination and Confluence of Rewriting
TACAS
Christian Sternagel University of Innsbruck, Austria, Akihisa Yamada
Link to publication