Program

Click on a title to view the paper or download it as a PDF to your device.


If you wish to download the complete volumes please click on the appropriate link below.
TACAS (Vol.1) - TACAS (Vol.2) - FoSSaCS - ESOP - POST - FASE


Overview Programme


Monday

Apr 16


08:00

Registration opens


08:30 - 09:00

ETAPS Opening
Alexandros I


09:00 - 10:00

Keynote Speech
Benjamin Pierce
Alexandros I


10:00 - 10:30

Coffee Break


10:30 - 12:30

TACAS
Alexandros I
FoSSaCS
Amfitrion I
ESOP
Aristotelis II
POST
Amfitrion II


12:30 - 14:00

Lunch


14:00 - 16:00

TACAS
Alexandros I
FoSSaCS
Amfitrion I
ESOP
Aristotelis II
POST
Amfitrion II


16:00 - 16:30

Coffee Break


16:30 - 18:00

TACAS
Aristotelis II
Invited Tutorial
Fabio Somenzi
Alexandros I


18:30 - 20:00

Reception
Hotel Lounge / Poolside



Tuesday

Apr 17


09:00 - 10:00

Keynote Speech
Martin Abadi
Alexandros I


10:00 - 10:30

Coffee Break


10:30 - 12:30

TACAS
Alexandros I
FoSSaCS
Amfitrion I
ESOP
Aristotelis II
POST
Amfitrion II


12:30 - 14:00

Lunch


14:00 - 16:00

TACAS
Alexandros I
FoSSaCS
Amfitrion I
ESOP
Aristotelis II
POST
Amfitrion II


16:00 - 16:30

Coffee Break


16:30 - 18:00

TACAS
Alexandros I
FoSSaCS
Amfitrion I
ESOP
Aristotelis II


Wednesday

Apr 18


09:00 - 10:00

Keynote Speech
Pamela Zave
Alexandros I


10:00 - 10:30

Coffee Break


10:30 - 12:30

TACAS
Alexandros I
FoSSaCS
Amfitrion I
ESOP
Aristotelis II
FASE
Amfitrion II


12:30 - 14:00

Lunch


14:00 - 16:00

TACAS
Alexandros I
FoSSaCS
Amfitrion I
ESOP
Aristotelis II
FASE
Amfitrion II


16:00 - 16:30

Coffee Break


16:30 - 18:00

TACAS
Aristotelis II
Invited Tutorial
Armin Biere, Johannes Kepler
Alexandros I


20:00

Conference Dinner
Kitchen Bar restaurant



Thursday

Apr 19


09:00 - 10:00

Keynote Speech
Derek Dreyer
Alexandros I


10:00 - 10:30

Coffee Break


10:30 - 12:30

TACAS
Alexandros I
FoSSaCS
Amfitrion I
ESOP
Aristotelis II
FASE
Amfitrion II


12:30 - 14:00

Lunch


14:00 - 16:00

TACAS
Alexandros I
TACAS
Amfitrion I
ESOP
Aristotelis II
FASE
Amfitrion II


16:00 - 16:30

Coffee Break


16:30 - 18:00

TACAS
Alexandros I
TACAS
SV-COMP Community Meeting
Amfitrion I
ESOP
Aristotelis II
FASE
Amfitrion II






Monday
16 April

08:00

Registration Opens


08:30 - 09:00

ETAPS Opening

Alexandros I
Joost-Pieter Katoen, Pericles A. Mitkas (Rector), Panagiotis Katsaros


09:00 - 10:00

Invited Speaker

Alexandros I
Benjamin Pierce, Un. of Pennsylvania, USA
Chairs: Lujo Bauer/Ralf Küsters


10:00 - 10:30

Coffee Break


10:30 - 12:30

TACAS

Theorem Proving

Alexandros I
Chair: Marieke Huisman

Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning
Giles Reger, Martin Suda and Andrei Voronkov

Efficient verification of imperative programs using auto2
Bohua Zhan

Frame Inference for Inductive Entailment Proofs in Separation Logic
Quang Loc Le, Jun Sun and Shengchao Qin

Verified Model Checking of Timed Automata
Simon Wimmer and Peter Lammich

FoSSaCS

Semantics

Amfitrion I
Chair: Radha Jagadeesan

Non-angelic concurrent game semantics
Simon Castellan, Pierre Clairambault, Jonathan Hayman and Glynn Winskel

A Trace Semantics for System F Parametric Polymorphism
Guilhem Jaber and Nikos Tzevelekos

Categorical combinatorics for non deterministic strategies on simple games
Clément Jacq and Paul-André Melliès

A Syntactic View of Computational Adequacy
Marco Devesas Campos and Paul Levy

ESOP

Language Design

Aristotelis II
Chair: Andreas Rossberg

Consistent Subtyping for All
Ningning Xie, Xuan Bi, Bruno C. d. S. Oliveira

HOBiT: Programming Lenses without using Lens Combinators
Kazutaka Matsuda and Meng Wang

Deterministic Concurrency: A Clock-Synchronised Shared Memory Approach
Joaquin Aguado, Michael Mendler, Marc Pouzet, Partha Roop, Reinhard von Hanxleden

Dualizing Generalized Algebraic Data Types by Matrix Transposition
Klaus Ostermann, Julian Jabs
* Authors will not be at ESOP to present the paper.

POST

Information Flow & Non-Interference

Amfitrion II
Chair: Lujo Bauer

What's the Over/ Under? Probabilistic Bounds on Information Leakage
Ian Sweet, Jose Calderon, Chad Scherrer, Michael Hicks and Stephen Magill

Secure Information Release in Timed Automata
Panagiotis Vasilikos, Flemming Nielson and Hanne Riis Nielson

Compositional Non-Interference for Concurrent Programs via Separation and Framing
Aleksandr Karbyshev, Kasper Svendsen, Aslan Askarov and Lars Birkedal

The Meaning of Memory Safety
Arthur Azevedo de Amorim, Catalin Hritcu and Benjamin Pierce


12:30 - 14:00

Lunch


14:00 - 16:00

TACAS

SAT & SMT I

Alexandros I
Chair: Rance Cleaveland

Chain Reduction for Binary and Zero-Suppressed Decision Diagrams
Randal Bryant

CDCLSym: Introducing Effective Symmetry Breaking in SAT Solving
Hakan Metin, Souheib Baarir, Maximilien Colange and Fabrice Kordon

Automatic Generation of Precise and Useful Commutativity Conditions
Kshitij Bansal, Eric Koskinen and Omer Tripp

Bit-Vector Model Counting using Statistical Estimation
Seonmo Kim and Stephen McCamant

FoSSaCS

Linearity

Amfitrion I
Chair: Luis Caires

A New Linear Logic for Deadlock-Free Session-Typed Processes
Ornela Dardha and Simon Gay

A Double-Category Theoretic Analysis of Graded Linear Exponential Comonads
Shin-Ya Katsumata

Depending on Session-Typed Processes
Bernardo Toninho and Nobuko Yoshida

FabULous Interoperability for ML and a Linear Language
Gabriel Scherer, Max New, Nicholas Rioux and Amal Ahmed

ESOP

Probabilistic Programming

Aristotelis II
Chair: Jan Hoffmann

An Assertion-Based Program Logic for Probabilistic Programs
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub

Fine-grained Semantics for Probabilistic Programs
Benjamin Bichsel, Timon Gehr, Martin Vechev

How long, O Bayesian network, will I sample thee?
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus
Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Aleš Bizjak, Marco Gaboardi, Deepak Garg

POST

Leakage, Information Flow, and Protocols

Amfitrion II
Chair: Aslan Askarov

Formal Verification of Integrity Preserving Countermeasures against Cache Storage
Hamed Nemati, Roberto Guanciale, Christoph Baumann and Mads Dam

Leakage and protocol composition in a game-theoretic perspective
Mario S. Alvim, Konstantinos Chatzikokolakis, Yusuke Kawamoto and Catuscia Palamidessi

Equivalence properties by typing in cryptographic branching protocols
Véronique Cortier, Niklas Grimm, Joseph Lallemand and Matteo Maffei

Design, Formal Specification and Analysis of Multi-Factor Authentication Solutions with a Single Sign-On Experience
Giada Sciarretta, Roberto Carbone, Silvio Ranise and Luca Viganò


16:00 - 16:30

Coffee Break


16:30 - 18:00

TACAS

Deductive Verification

Aristotelis II
Chair: Damien Zufferey

Hoare Logics for Time Bounds
Maximilian Paul Louis Haslbeck and Tobias Nipkow

A Verified Implementation of the Bounded List Container
Raphaël Cauderlier and Mihaela Sighireanu

Automating Deductive Verification for Weak-Memory Programs
Alexander J. Summers and Peter Müller

Invited Tutorial

Alexandros I

Fabio Somenzi, Un. of Colorado, Boulder, USA


18:30 - 20:00

Reception
Hotel Lounge / Poolside



Tuesday
17 April

09:00 - 10:00

Invited Speaker

Alexandros I
Martin Abadi, Google Brain, USA
Chair: Joost-Pieter Katoen


10:00 - 10:30

Coffee Break


10:30 - 12:30

TACAS

Software Verification and Optimization

Alexandros I
Chair: Tomáš Vojnar

Property Checking Array Programs Using Loop Shrinking
Shrawan Kumar, Amitabha Sanyal, Venkatesh R and Punit Shah

Invariant Synthesis for Incomplete Verification Engines
Daniel Neider, P. Madhusudan, Pranav Garg, Shambwaditya Saha and Daejun Park

Accelerating Syntax-Guided Invariant Synthesis
Grigory Fedyukovich and Rastislav Bodik

Daisy - Framework for Analysis and Optimization of Numerical Programs (Tool Paper)
Eva Darulova, Anastasiia Izycheva, Fariha Nasir, Fabian Ritter, Heiko Be-cker and Robert Bastian

FoSSaCS

Concurrency

Amfitrion I
Chair: Catuscia Palamidessi

Automata for True Concurrency Properties
Paolo Baldan and Tommaso Padoan

A Theory of Encodings and Expressiveness
Rob van Glabbeek

A Framework for Parameterized Monitorability
Luca Aceto, Antonis Achilleos, Adrian Francalanza and Anna Ingolfsdottir

Logics for Bisimulation and Divergence
Xinxin Liu, Tingting Yu and Wenhui Zhang

ESOP

Types and Effects

Aristotelis II
Chair: Gabriel Scherer

Failure is Not an Option: An Exceptional Type Theory
Pierre-Marie Pédrot, Nicolas Tabareau

Let Arguments Go First
Ningning Xie, Bruno C. d. S. Oliveira

Behavioural equivalence via modalities for algebraic effects
Alex Simpson, Niels Voorneveld

Explicit Effect Subtyping
Amr Hany Saleh, Georgios Karachalias, Matija Pretnar, Tom Schrijvers

POST

Smart Contracts and Privacy

Amfitrion II
Chair: Ralf Küsters

SoK: unraveling Bitcoin smart contracts
Nicola Atzei, Massimo Bartoletti, Tiziana Cimoli, Stefano Lande and Roberto Zunino

A Semantic Framework for the Security Analysis of Ethereum smart contracts
Ilya Grishchenko, Matteo Maffei and Clara Schneidewind

Tool Demonstration: FSolidM for Designing Secure Ethereum Smart Contracts
Anastasia Mavridou and Aron Laszka

UniTraX: Protecting Data Privacy with Discoverable Biases
Reinhard Munz, Fabienne Eigner, Matteo Maffei, Paul Francis and Deepak Garg


12:30 - 14:00

Lunch


14:00 - 16:00

TACAS

Model Checking

Alexandros I
Chair: Armin Biere

Oink: an Implementation and Evaluation of Modern Parity Game Solvers
Tom van Dijk

More Scalable LTL Model Checking via Discovering Design-Space Dependencies
Rohit Dureja and Kristin Yvonne Rozier

Generation of Minimum Tree-like Witnesses for Existential CTL
Chuan Jiang and Gianfranco Ciardo

From Natural Projection to Partial Model Checking and Back
Gabriele Costa, David Basin, Chiara Bodei, Pierpaolo Degano and Letterio Galletta

FoSSaCS

Lambda Calculus and Types

Amfitrion I
Chair: Alex Simpsom

Call-by-need, neededness and all that
Delia Kesner, Alejandro Rios and Andres Viso

Fitch-Style Modal Lambda Calculi
Ranald Clouston

Realizability interpretation and normalization of typed call-by-need λ-calculus with control
Étienne Miquey and Hugo Herbelin

Quotient Inductive-Inductive Types
Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Nicolai Kraus and Fredrik Nordvall Forsberg

ESOP

Concurrency

Aristotelis II
Chair: Limin Jia

A separation logic for a promising semantics
Kasper Svendsen, Jean Pichon-Pharabod, Marko Doko, Ori Lahav, Viktor Vafeiadis

Logical Reasoning for Disjoint Permissions
Xuan Bach Le, Aquinas Hobor

Deadlock-Free Monitors
Jafar Hamin, Bart Jacobs

Fragment Abstraction for Concurrent Shape Analysis
Parosh Aziz Abdulla, Bengt Jonsson, Cong Quy Trinh

POST

Firewalls and Attack-Defense Trees

Amfitrion II
Chair: Matteo Maffei

Transcompiling Firewalls
Chiara Bodei, Pierpaolo Degano, Riccardo Focardi, Letterio Galletta and Mauro Tempesta

On quantitative analysis of attack-defense trees with repeated labels
Barbara Kordy and Wojciech Widel


16:00 - 16:30

Coffee Break


16:30 - 18:00

TACAS

Machine Learning

Alexandros I
Chair: Bernhard Steffen

ICE-based Refinement Type Discovery for Higher-Order Functional Programs
Adrien Champion, Tomoya Chiba, Naoki Kobayashi and Ryosuke Sato

Strategy Representation by Decision Trees in Reactive Synthesis
Tomas Brazdil, Krishnendu Chatterjee, Jan Kretinsky and Viktor Toman

Feature-Guided Black-Box Safety Testing of Deep Neural Networks
Matthew Wicker, Xiaowei Huang and Marta Kwiatkowska

FoSSaCS

Category Theory and Quantum Control

Amfitrion I
Chair: Ichiro Hasuo

Guarded Traced Symmetric Monoidal Categories
Sergey Goncharov and Lutz Schröder

Proper Semirings and Proper Convex Functors
Ana Sokolova and Harald Woracek

From Symmetric Pattern-Matching to Quantum Control
Amr Sabry, Juliana Vizzotto and Benoît Valiron

ESOP

Security

Aristotelis II
Chair: Deepak Garg

Reasoning About a Machine with Local Capabilities - Provably Safe Stack and Return Pointer Management
Lau Skorstengaard, Dominique Devriese, Lars Birkedal

Modular Product Programs
Marco Eilers, Peter Müller, Samuel Hitz


Wednesday
18 April

09:00 - 10:00

Invited Speaker

Alexandros I
Pamela Zave, AT&T Labs, USA
Chair: Alessandra Russo


10:00 - 10:30

Coffee Break


10:30 - 12:30

TACAS

Concurrent and Distributed Systems

Alexandros I
Chair: Lijun Zhang

Computing the concurrency threshold of sound free-choice workflow nets
Philipp J. Meyer, Javier Esparza and Hagen Völzer

Fine-Grained Complexity of Safety Verification
Peter Chini, Roland Meyer and Prakash Saivasan

Parameterized verification of synchronization in constrained reconfigurable broadcast networks
Balasubramanian A.R., Nathalie Bertrand and Nicolas Markey

EMME: a formal tool for the ECMAScript Memory Model Evaluation
Cristian Mattarei, Clark Barrett, Shu-Yu Guo, Bradley Nelson and Ben Smith

FoSSaCS

Quantitative Models

Amfitrion I
Chair: Ugo Dal Lago

The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes
Stéphane Le Roux and Guillermo Pérez

A Hierarchy of Scheduler Classes for Stochastic Automata
Pedro R. D'Argenio, Marcus Gerhold, Arnd Hartmanns and Sean Sedwards

Symbolically Quantifying Response Time in Stochastic Models using Moments and Semirings
Hugo Bazille, Eric Fabre and Blaise Genest

Comparator Automata in Quantitative Verification
Suguman Bansal, Swarat Chaudhuri and Moshe Vardi

ESOP

Program Verification

Aristotelis II
Chair: Ilya Sergey

A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program Verification
Armaël Guéneau, Arthur Charguéraud, François Pottier

Verified Learning Without Regret
Samuel Merten, Alexander Bagnall, Gordon Stewart

Program Verification by Coinduction
Brandon Moore, Lucas Peña, Grigore Rosu

Velisarios: Byzantine Fault Tolerant Protocols Powered by Coq
Vincent Rahli, Ivana Vukotic, Marcus Volp, Paulo Verissimo

FASE

Model-Based Software Development

Amfitrion II
Chair: Wil van der Aalst

A Formal Framework for Incremental Model Slicing
Gabriele Taentzer, Timo Kehrer, Christopher Pietsch and Udo Kelter

Multiple Model Synchronization with Multiary Delta Lenses
Zinovy Diskin, Harald König and Mark Lawford

Controlling the Attack Surface of Object-Oriented Refactorings
Sebastian Ruland, Géza Kulcsár, Erhan Leblebici, Sven Peldszus and Malte Lochau

Effective Analysis of Attack Trees: a Model-Driven Approach
Rajesh Kumar, Stefano Schivo, Enno Ruijters, Bugra Mehmet Yildiz, David Huistra, Jacco Brandt, Arend Rensink and Mariëlle Stoelinga


12:30 - 14:00

Lunch


14:00 - 16:00

TACAS

SAT & SMT

Alexandros I
Chair: Matthias Heizmann

What a Difference a Variable Makes
Marijn Heule and Armin Biere

Abstraction Refinement for Emptiness Checking of Alternating Data Automata
Radu Iosif and Xiao Xu

Revisiting Enumerative Instantiation
Andrew Reynolds, Haniel Barbosa and Pascal Fontaine

An Non-linear Arithmetic Procedure for Control-Command Software Verification
Pierre Roux, Mohamed Iguernlala and Sylvain Conchon

FoSSaCS

Logics and Equational Theories

Amfitrion I
Chair: Alexandra Silva

Modular Tableaux Calculi for Separation Theories
Simon Docherty and David Pym

Differential Calculus with Imprecise Input and its Logical Framework
Abbas Edalat and Mehrdad Maleki

The Effects of Adding Reachability Predicates in Propositional Separation Logic
Stéphane Demri, Étienne Lozes and Alessio Mansutti

The equational theory of the natural join and of inner union is decidable
Luigi Santocanale

ESOP

Program Analysis and Automated Verification

Aristotelis II
Chair: Jan Kofron

Evaluating Design Tradeoffs in Numeric Static Analysis for Java
Shiyi Wei, Piotr Mardziel, Andrew Ruef, Jeffrey S. Foster, Michael Hicks

An Abstract Interpretation Framework for Input Data Usage
Caterina Urban, Peter Müller

Higher-Order Program Verification via HFL Model Checking
Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe

Quantitative Analysis of Smart Contracts
Krishnendu Chatterjee, Amir Kafshdar Goharshady, Yaron Velner

FASE

Distributed Program and System Analysis

Amfitrion II
Chair: Marsha Chechik

ROLA: A New Distributed Transaction Protocol and Its Formal Analysis
Si Liu, Peter Ölveczky, Keshav Santhanam, Qi Wang, Indranil Gupta and Jose Meseguer

A Process Network Model for Reactive Streaming Software with Deterministic Task Parallelism
Fotios Gioulekas, Peter Poplavko, Panagiotis Katsaros, Saddek Bensa-lem and Pedro Palomo

Distributed Graph Queries for Runtime Monitoring of Cyber-Physical Systems
Márton Búr, Gábor Szilágyi, András Vörös and Daniel Varro

EventHandler-based Analysis Framework for Web Apps using Dynamically Collected States
Joonyoung Park, Kwangwon Sun and Sukyoung Ryu


16:00 - 16:30

Coffee Break


16:30 - 18:00

TACAS

Security & Reactive Systems

Aristotelis II
Chair: Tiziana Margaria

Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection
Milan Ceska, Vojtech Havlena, Lukas Holik, Ondrej Lengal and Tomas Vojnar

Validity-Guided Synthesis of Reactive Systems from Assume - Guarantee Contract
Andreas Katis, Grigory Fedyukovich, Huajun Guo, Andrew Gacek, John Backes, Arie Gurfinkel and Michael Whalen

RVHyper: A Runtime Verification Tool for Temporal Hyperproperties (tool demo)
Bernd Finkbeiner, Christopher Hahn, Marvin Stenger and Leander Tentrup

The Refinement Calculus of Reactive Systems Toolset (tool demo)
Iulia Dragomir, Viorel Preoteasa and Stavros Tripakis

Invited Tutorial

Alexandros I

Armin Biere, Johannes Kepler University, Linz, Austria


20:00

Conference Dinner
Kitchen Bar restaurant



Thursday
19 April

09:00 - 10:00

Invited Speaker

Alexandros I
Derek Dreyer, MPI-SWS, Germany
Chair: Amal Ahmed


10:00 - 10:30

Coffee Break


10:30 - 12:30

TACAS

Static and Dynamic Program Analysis

Alexandros I
Chair: Dirk Beyer

TESTOR: A Modular Tool for On-the-Fly Conformance Test Case Generation
Lina Marsso, Radu Mateescu and Wendelin Serwe

Optimal Dynamic Partial Order Reduction with Observers
Stavros Aronis, Bengt Jonsson, Magnus Lång and Konstantinos Sagonas

Structurally Defined Conditional Data-flow Static Analysis
Elena Sherman and Matthew Dwyer

Geometric Nontermination Arguments
Jan Leike and Matthias Heizmann

FoSSaCS

Graphs and Automata

Amfitrion I
Chair: Nathalie Bertrand

Minimization of Graph Weighted Models over Circular Strings
Guillaume Rabusseau

Games on graphs with a public signal monitoring
Patricia Bouyer

WQO Dichotomy for 3-graphs
Sławomir Lasota and Radosław Piórkowski

Verifying Higher-Order Functions with Tree Automata
Thomas Genet, Timothée Haudebourg and Thomas Jensen

ESOP

Session Types and Concurrency

Aristotelis II
Chair: Luis Caires

Session-Typed Concurrent Contracts
Hannah Gommerstadt, Limin Jia, Frank Pfenning

A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems
Malte Viering, Tzu-Chun Chen, Patrick Eugster, Raymond Hu, Lukasz Ziarek

On Polymorphic Sessions and Functions: A Tale of Two (Fully Abstract) Encodings
Bernardo Toninho, Nobuko Yoshida

Concurrent Kleene Algebra: Free Model and Completeness
Tobias Kappé, Paul Brunet, Alexandra Silva, Fabio Zanasi

FASE

Software Design and Verification

Amfitrion II
Chair: Marieke Huisman

Hierarchical Specification and Verification of Architecture Design Patterns
Diego Marmsoler

Supporting Verification-Driven Incremental Distributed Design of Components
Claudio Menghi, Paola Spoletini, Marsha Chechik and Carlo Ghezzi

Summarizing Software API Usage Examples using Clustering Techniques
Nikolaos Katirtzis, Themistoklis Diamantopoulos and Charles Sutton

Fast Computation of Arbitrary Control Dependencies
Jean-Christophe Léchenet, Nikolai Kosmatov and Pascale Le Gall


12:30 - 14:00

Lunch


14:00 - 16:00

TACAS

Hybrid and Stochastic Systems

Alexandros I
Chair: Goran Frehse

Efficient dynamic error reduction for hybrid systems reachability analysis
Stefan Schupp and Erika Abraham

AMT2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic
Dejan Nickovic, Olivier Lebeltel, Oded Maler, Thomas Ferrère and Dogan Ulus

Multi-Cost Bounded Reachability in MDPs
Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen and Tim Quatmann

A Statistical Model Checker for Nondeterminism and Rare Events
Carlos E. Budde, Pedro R. D'Argenio, Arnd Hartmanns and Sean Sedwards

TACAS / SV-COMP

Competition on Software Verification

Amfitrion I

List of Presentations

ESOP

Concurrency and Distribution

Aristotelis II
Chair: Naoki Kobayashi

Correctness of a Concurrent Object Collector for Actor Languages
Juliana Vicente Franco, Sylvan Clebsch, Sophia Drossopoulou, Jan Vitek, Tobias Wrigstad

Paxos Consensus, Deconstructed and Abstracted
Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman, Ilya Sergey

On Parallel Snapshot Isolation and Release/Acquire Consistency
Azalea Raad, Ori Lahav, Viktor Vafeiadis

Eventual Consistency for CRDTs
Radha Jagadeesan, James Riely

FASE

Specification and Program Testing

Amfitrion II
Chair: Julia Rubin

Iterative Generation of Diverse Models for Testing Specifications of DSL Tools
Oszkár Semeráth and Daniel Varro

Optimising Spectrum Based Fault Localisation for Single Fault Programs using Specifications
David Landsberg, Youcheng Sun and Daniel Kroening

TCM: Test Case Mutation to Improve Crash Detection in Android
Yavuz Koroglu and Alper Sen

CRETE: A Versatile Binary-Level Concolic Testing Framework
Bo Chen, Christopher Havlicek, Zhenkun Yang, Kai Cong, Raghudeep Kannavara and Fei Xi


16:00 - 16:30

Coffee Break


16:30 - 18:00

TACAS

Temporal Logic and Mu-Calculus

Alexandros I
Chair: Marieke Huisman

Permutation Games for the Weakly Aconjunctive mu-Calculus
Daniel Hausmann, Lutz Schröder and Hans-Peter Deifel

Symmetry Reduction for the Local Mu-Calculus
Kedar Namjoshi and Richard Trefler

Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models
Luca Bortolussi and Simone Silvetti

TACAS

Competition on Software Verification

Amfitrion I

SV-COMP Community Meeting

ESOP

Compiler Verification

Aristotelis II
Chair: Xavier Leroy

A Verified Compiler from Isabelle/HOL to CakeML
Lars Hupel, Tobias

Compositional Verification of Compiler Optimisations on Relaxed Memory
Mike Dodds, Mark Batty, Alexey Gotsman

FASE

Family-Based Software Development

Amfitrion II
Chair: Gabi Taentzer

Abstract Family-based Model Checking using Modal Featured Transition Systems: Preservation of CTL*
Aleksandar S. Dimovski

FPH: Efficient Non-Commutativity Analysis of Feature-Based Systems
Marsha Chechik, Ioanna Stavropoulou, Cynthia Disenfeld and Julia Rubin

Taming Multi-Variability of Software Product Line Transformations
Daniel Strüber, Sven Peldszus and Jan Jürjens




7th Intl. Competition on Software Verification held at TACAS 2018

Overview of the Competition and Message from the Organizer

Tomas Vojnar
  1. 2LS: Memory Safety and Non-Termination
Viktor Malik, Štefan Martiček, Peter Schrammel, Mandayam Srivas, Tomas Vojnar and Johanan Wahlang
  1. CBMC -- C Bounded Model Checker
Lucas Cordeiro, Daniel Kroening, Peter Schrammel, Michael Tautschnig and Marek Trtik
  1. CPA-BAM-BnB: Block-Abstraction Memoization and Region-based Memory Models for Predicate Abstractions
Pavel Andrianov, Vadim Mutilin, Karlheinz Friedberger, Mikhail Mandrykin and Anton Volkov
  1. CPA-BAM-Slicing: Block-Abstraction Memoization for Predicate Abstractions and Slicing with Region-Based Dependency Analysis
Pavel Andrianov, Vadim Mutilin, Mikhail Mandrykin and Anton Vasilyev
  1. CPAchecker for Reachability, Memory Safety, Overflows, Concurrency, and Termination
Matthias Dangl, Karlheinz Friedberger, Marie-Christine Jakobs, Thomas Lemberger and Philipp Wendler
  1. ESBMC
Mikhail Ramalho, Jeremy Morse, Lucas Cordeiro, Bernd Fischer, Denis Nicole, Hussama Ismail and Felipe Rodriguez
  1. InterpChecker: Reducing State Space via Interpolations
Zhao Duan, Cong Tian, Zhenhua Duan and Luke Ong
  1. Map2Check using LLVM and KLEE
Rafael Menezes, Herbert Rocha, Lucas Cordeiro and Raimundo Barreto
  1. Symbiotic 5: Boosted Instrumentation
Marek Chalupa, Martina Vitovská and Jan Strejček
  1. Ultimate Automizer and the Search for Perfect Interpolants
Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Betim Musa, Alexander Nutz, Christian Schilling, Tanja Schindler and Andreas Podelski
  1. Ultimate Kojak
Daniel Dietsch, Marius Greitschus, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski, Christian Schilling and Tanja Schindler
  1. Ultimate Taipan with Dynamic Block Encoding
Daniel Dietsch, Marius Greitschus, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz, Andreas Podelski, Christian Schilling and Tanja Schindler
  1. VeriAbs : Verification by Abstraction and Test Generation
Priyanka Darke, Sumanth Prabhu, Bharti Chimdyalwar, Avriti Chauhan, Shrawan Kumar, Animesh Basakchowdhury, Venkatesh R, Advaita Datar and Raveendra Kumar Medicherla
  1. Yogar-CBMC: CBMC with Scheduling Constraint Based Abstraction Refinement
Liangze Yin, Wei Dong, Wanwei Liu, Yunchou Li and Ji Wang