Programme
Programme of main conferences from Monday to Thursday. Best Paper candidates are highlighted in yellow and by asterisk.
Thursday 27 April
9:00
Sven Apel: Brains on Code: Towards a Neuroscientific Foundation of Program Comprehension (FASE invited talk)
Chair: Leen Lambers
Room: Auditorium
10:00
Coffee break
Room: Foyer + 44 lobby
TACAS: Verification II
Chair: Dirk Beyer
Room: Auditorium
10:30
Make flows small again: revisiting the flow framework
Roland Meyer, Thomas Wies and Sebastian Wolff
11:00
ALASCA: Reasoning in Quantified Linear Arithmetic
Johannes Schoisswohl, Laura Kovacs, Giles Reger, Konstantin Korovin and Andrei Voronkov
11:30
A Matrix-Based Approach to Parity Games
Saksham Aggarwal, Alejandro Stuckey de la Banda, Henri Urpani, Luke Yang and Julian Gutierrez
12:00
A GPU Tree Database for Many-Core Explicit State Space Exploration
Anton Wijs and Muhammad Osama
TACAS: Graphs/Probabilistic Systems
Chair: Natasha Sharygina
Room: 44-45/108
10:30
A Truly Symbolic Linear-Time Algorithm for SCC Decomposition
Casper Abild Larsen, Simon Meldahl Schmidt, Jesper Steensgaard, Anna Blume Jakobsen, Jaco van de Pol and Andreas Pavlogiannis
11:00
Transforming quantified boolean formulas using biclique covers
Oliver Kullmann and Ankit Shukla
11:30
Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration
T. Winkler, Joost-Pieter Katoen
12:00
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
K. Batz, M. Chen, S. Junges, B. Kaminski, Joost-Pieter Katoen, Christoph Matheja
FASE: Analysis & Verification
Chair: Eduard Kamburjan
Room: 44-54/109
10:30
Parallel Program Analysis via Range Splitting
Jan Haltermann, Marie-Christine Jakobs, Cedric Richter and Heike Wehrheim
11:00
Yet Another Model! A Study on Model's Similarities for Defect and Code Smells
Geanderson Santos, Amanda Santana, Gustavo Vale and Eduardo Figueiredo
11:30
A Modeling Concept for Formal Verification of OS-Based Compositional Software
Leandro Batista Ribeiro, Florian Lorber, Ulrik Nyman, Kim Guldstrand Larsen and Marcel Baunach
12:00
Towards Log Slicing (NIER paper)
Joshua Dawes, Donghwan Shin and Domenico Bianculli
12:15
JavaBIP meets VerCors: Towards the Safety of Concurrent Software Systems in Java (Tool paper)
Simon Bliudze, Petra van den Bos, Marieke Huisman, Robert Rubbens and Larisa Safina
FoSSaCS: Verification
Chair:
Room: 44-45/106
10:30
Just Testing
Rob van Glabbeek
11:00
Model and Program Repair via Group Actions
William Cocke and Paul Attie
11:30
Subgame optimal strategies in finite concurrent games with prefix-independent objectives
Benjamin Bordais, Patricia Bouyer and Stephane Le Roux.
SPIN (co-located)
Chair: Sergio Mover
Room: 25-26/105
11:30
Efficient Trace Generation for Rare-Event Analysis in Chemical Reaction Networks
Bryant Israelsen, Landon Taylor and Zhen Zhang
12:00
Accelerating black box testing with light-weight learning
Roi Fogler, Itay Cohen and Doron Peled
12:30
Lunch
Room: Patio + Foyer
TACAS: Model Checking II
Chair: Sriram Sankaranarayanan
Room: Auditorium
14:00
Optimal Stateless Model Checking for Causal Consistency
Parosh Abdulla, Mohamed Faouzi Atig, Krishna S, Ashutosh Gupta and Omkar Tuppe
14:30
Symbolic Model Checking for TLA+ Made Faster
R. Otoni, I. Konnov, J. Kukovec, P. Eugster, N. Sharygina
15:00
AutoHyper: Explicit-State Model Checking for HyperLTL*
R. Beutner and B. Finkbeiner
FASE: Testing
Chair: Andrzej Wąsowski
Room: 44-45/108
14:00
Efficient Bounded Exhaustive Input Generation from Program APIs
Mariano Politano, Valeria Bengolea, Facundo Molina, Nazareno Aguirre, Marcelo Frias and Pablo Ponzio
14:30
Model-based Player Experience Testing with Emotion Pattern Verification
Saba Gholizadeh Ansari, I. S. W. B. Prasetya, Davide Prandi, Fitsum Meshesha Kifetew, Frank Dignum, Mehdi Dastani and Gabriele Keller
15:00
Concolic Testing of Front-end JavaScript
Zhe Li and Fei Xie
Awards
Chair: Marieke Huisman
Room: 44-45/106
14:00
Test-of-Time Award
Explicit-State Software Model Checking Based on CEGAR and Interpolation, by Dirk Beyer and Stefan Löwe
14:30
Dissertation Award
Pushing the Barriers in Controller Synthesis for Cyber-Physical Systems, by Kaushik Mallik
15:00
Test-of-Time Tool Award
CADP: Construction and Analysis of Distributed Processes, by Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe
SPIN (co-located)
Chair: Matthias Heizmann
Room: 25-26/105
15:00
WikiCoder: Learning to Write Knowledge-Powered Code
Théo Matricon, Nathanaël Fijalkow and Gaëtan Margueritte
15:30
Provable Correct and Adaptive Simplex Architecture for Bounded-Liveness Properties
Benedikt Maderbacher, Stefan Schupp, Ezio Bartocci, Roderick Bloem, Dejan Nickovic and Bettina Könighofer
16:00
Coffee break
Room: Foyer + 44 lobby
TACAS: Monitoring/Program Analysis
Chair: Jan Kofroň
Room: Auditorium
16:30
Industrial-Strength Controlled Concurrency Testing for C# Programs with Coyote*
P. Deligiannis, A. Senthilnathan, F. Nayyar, C. Lovett, A. Lal
17:00
Context-Sensitive Meta-Constraint Systems for Explainable Program Analysis
Kalmer Apinis and Vesal Vojdani
17:30
Explainable Online Monitoring of Metric Temporal Logic
L. Lima, A. Herasimau, M. Raszyk, D. Traytel, S. Yuan
TACAS: Synthesis II
Chair: Cesar Sanchez
Room: 44-45/108
16:30
Synthesis of Distributed Agreement-Based Systems with Efficiently-Decidable Verification*
N. Jaber, C. Wagner, S. Jacobs, M. Kulkarni, R. Samanta
17:00
LTL Reactive Synthesis with a Few Hints
M. Balachander, E. Filiot, Jean-Francois Raskin
17:30
Timed Automata Verification and Synthesis via Finite Automata Learning
Ocan Sankur
FASE: Test-Comp
Chair: Dirk Beyer
Room: 24-25/405
16:30
Organization
Dirk Beyer
16:50
FuSeBMC_IA
Fedor Shmarov
17:05
Legion
Gidon Ernst
17:20
VeriFuzz
M. Raveemdra Kumar
17:35
Community Meeting
Dirk Beyer