ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
You're viewing the program in a time zone which is different from your device's time zone change time zone

Sat 6 Apr

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

09:00 - 10:30
09:00
60m
Talk
Invited talk by Margus Veanes
PERR
Margus Veanes Microsoft Research
10:00
30m
Talk
Local Reasoning for Robust Observational Equivalence
PERR
Dan Ghica University of Birmingham, Koko Muroya RIMS, Kyoto University, JP & University of Birmingham, UK, Todd Waugh Ambridge University of Birmingham
09:00 - 10:30
IDICE-FOPARA at S11
Chair(s): Steffen Jost LMU, Munich, Germany
09:45
45m
Talk
PRAMs over integers do not compute maxflow efficiently
DICE-FOPARA
09:00 - 10:30
IGaLoP at S3
09:00
60m
Talk
Intertwining game theory and game semantics
GaLoP
I: Jules Hedges University of Oxford
10:00
30m
Talk
Universal property of the monad for infinite trace strategies (work in progress)
GaLoP
Paul Blain Levy University of Birmingham, Sergey Goncharov FAU Erlangen-Nürnberg, Lehrstuhl 8, Lutz Schröder FAU Erlangen-Nürnberg, Lehrstuhl 8
09:00 - 10:30
Mechanising Proofs for Behavioural Types and ProcessesBEHAPI at S4 (BEHAPI)
Chair(s): António Ravara NOVA University of Lisbon and NOVA LINCS
09:00
30m
Talk
A Theory of Contexts for Higher-Order Encodings of Process Algebras
BEHAPI
Ivan Scagnetto University of Udine
09:30
30m
Talk
Formalising session-typed languages without worries
BEHAPI
Wen Kokke University of Edinburgh
10:00
30m
Talk
Adventures in Formalising the Meta-Theory of Session Types
BEHAPI
Francisco Ferreira Imperial College London
09:00 - 10:30
CoCoTOOLympics at S5
09:00 - 10:30
Welcome & Keynote 1MeTRiD at S510
Chair(s): Simon Bliudze INRIA Lillle - Nord Europe, Panagiotis Katsaros ITI-CERTH, Thessaloniki
09:15
15m
Day opening
Welcome
MeTRiD
Simon Bliudze INRIA Lillle - Nord Europe, Panagiotis Katsaros ITI-CERTH, Thessaloniki
09:30
60m
Talk
The Role of Models as Digital Twins of Smart Processes, Machines and Parts in Industry 4.0
MeTRiD
Tiziana Margaria University of Limerick and Lero - The Irish Software Research Centre
09:00 - 10:30
09:00
30m
Talk
Welcome to InterAVT 2019
InterAVT
Stylianos Basagiannis United Technologies Research centre, Goetz Botterweck Lero - The Irish Software Research Centre and University of Limerick, Anila Mjeda Lero - The Irish Software Research Centre and University of Limerick
09:30
30m
Talk
Invited Talk - "End-to-End Verification of Intelligent Cyber-Physical Systems: Progress and Challenges"
InterAVT
Nathan Fulton MIT-IBM Watson AI Lab
10:00
10m
Talk
Cross Programming Language Taint Analysis for the IoT Ecosystem
InterAVT
Pietro Ferrara JuliaSoft SRL, Italy, Amit Kr Mandal Università Ca' Foscari, Venezia, Italy, Agostino Cortesi Università Ca' Foscari Venezia, Fausto Spoto U. Verona
10:10
10m
Talk
FVL: Formal Verification in the Loop to Enhance Verification of Safety-Critical Cyber-Physical Systems
InterAVT
Cinzia Bernardeshi Univ. of Pisa, Andrea Domenici University of Pisa, Italy, Sergio Saponara University of Pisa, Italy
10:20
10m
Talk
Rigorous Design of FDIR Systems with BIP
InterAVT
09:00 - 10:30
IHSB at S9
Chair(s): Milan Ceska Brno University of Technology
09:00
10m
Day opening
Opening
HSB

09:10
60m
Talk
Invited talk: Modelling and personalisation techniques for behavioural prediction and emotion recognition
HSB
Marta Kwiatkowska University of Oxford
10:10
10m
Short-paper
Poster flash: Comprehensive Modelling Platform
HSB
Matej Troják Masaryk University, David Safranek Masaryk University, Jan Červený Global Change Research Institute CAS, Marek Havlík Masaryk University, Lukrécia Mertová Masaryk University, Matej Hajnal Masaryk University, Jakub Hrabec Masaryk University, Jakub Šalagovič Masaryk University
10:20
10m
Short-paper
Poster flash: Formalizing metabolic-regulatory networks by hybrid automata
HSB
Lin Liu Freie Universität Berlin, Alexander Bockmayr Freie Universität Berlin
09:00 - 10:30
VerifyThis 1 (Opening and event presentation)TOOLympics at SU2
09:00 - 10:30
10:30 - 16:00
Workshop Poster Exhibition (Saturday)Posters at Coffee area (Posters)
Chair(s): Jan Kofroň Charles University
10:30
22m
Poster
Markovian equivalences for biochemical reaction networks
Posters
Isabel Cristina Perez-Verona IMT Institute for Advanced Studies Lucca, Italy, Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy, Max Tschaikowski IMT Institute for Advanced Studies Lucca, Italy, Andrea Vandin DTU, Denmark, Luca Cardelli Microsoft Research and University of Oxford
10:52
22m
Poster
Statistical abstraction for multi-scale spatio-temporal systems
Posters
Michalis Michaelides University of Edinburgh, Jane Hillston University of Edinburgh, Guido Sanguinetti University of Edinburgh
11:14
22m
Poster
Towards Efficient Algorithms for Constraint Satisfaction Problems
Posters
Huu-Phuc Vo Uppsala University
11:36
22m
Poster
VIAP 1.1
Posters
11:58
22m
Poster
FreeST: context-free session types in a functional language
Posters
Bernardo Almeida Universidade de Lisboa, Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos University of Lisbon, Portugal
12:20
22m
Poster
WAPS: Weighted and Projected Sampling
Posters
Rahul Gupta , Shubham Sharma , Subhajit Roy IIT Kanpur, India, Kuldeep S. Meel National University of Singapore
12:42
22m
Poster
Semantic Fault Localization and Suspiciousness Ranking
Posters
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
13:04
22m
Poster
Ultimate Automizer
Posters
Matthias Heizmann University of Freiburg, Yu-Fang Chen Academia Sinica, Daniel Dietsch University of Freiburg, Marius Greitschus , Jochen Hoenicke Universität Freiburg, Yong Li Institute of Software, Chinese Academy of Sciences, Alexander Nutz University of Freiburg, Germany, Pavel Andrianov , Christian Schilling IST Austria, Tanja Schindler University of Freiburg, Andreas Podelski University of Freiburg, Germany
13:26
22m
Poster
CPAchecker with Strategy Selection
Posters
13:48
22m
Poster
Towards A Logical Account of Epistemic Causality
Posters
14:10
22m
Poster
Minimal-Time Synthesis for Parametric Timed Automata
Posters
Étienne André LIPN, CNRS UMR 7030, Université Paris 13, Vincent Bloemen University of Twente, Laure Petrucci Université Paris 13, Jaco van de Pol Aarhus University
14:32
22m
Poster
PeSCo: Predicting Sequential Combinations of Verifiers
Posters
Pavel Andrianov , Heike Wehrheim Paderborn University
14:54
22m
Poster
CoVeriTest: Cooperative Verifier-Based Testing
Posters
Dirk Beyer LMU Munich, Marie-Christine Jakobs TU Darmstadt, Germany
15:16
22m
Poster
JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)
Posters
Lucas Cordeiro University of Oxford, Daniel Kroening University of Oxford, Peter Schrammel University of Oxford, UK
15:38
22m
Poster
CPALockator: Thread-Modular Approach with Transition Abstraction for Analysis of Multithreaded Software
Posters
10:30 - 12:00
Morning BMooly Fest at JUPITER
10:30
30m
Talk
The Dilemma of Shape Analysis
Mooly Fest
Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc.
11:00
30m
Talk
Data Representation Synthesis: Past, Present and Future
Mooly Fest
Alex Aiken Stanford University
11:30
30m
Talk
Mooly: Mensch, Marathon, Method, Magic
Mooly Fest
Thomas Ball Microsoft Research
11:00 - 12:00
Timed systemsSynCoP at S10
11:00
45m
Talk
On Parameterised Jobshop Scheduling Problems
SynCoP
11:00 - 12:00
IIDICE-FOPARA at S11
Chair(s): Steffen Jost LMU, Munich, Germany
11:00
45m
Talk
Towards a Sheaf-Theoretic Definition of Decision Problems
DICE-FOPARA
11:00 - 12:00
IIGaLoP at S3
11:00
30m
Talk
Characterizing Downwards Closed Strongly First Order Dependencies
GaLoP
Pietro Galliani Free University of Bozen-Bolzano
11:30
30m
Talk
Logics for first-order definable team properties
GaLoP
Juha Kontinen , Fan Yang University of Helsinki
11:00 - 12:00
Mechanising Proofs of Behavioural Types for APIsBEHAPI at S4 (BEHAPI)
Chair(s): Luca Padovani University of Turin
11:00
20m
Talk
Proving properties about Linear Pi in Coq
BEHAPI
António Ravara NOVA University of Lisbon and NOVA LINCS, Marco Giunti NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
11:20
20m
Talk
Binary Session Types in Coq
BEHAPI
Ornela Dardha University of Glasgow
11:40
20m
Talk
Mechanise your proofs in Coq: From zero to cut-admissibility in less than three months.
BEHAPI
Marco Carbone IT University of Copenhagen
11:00 - 12:30
SL-COMPTOOLympics at S5
11:00 - 12:30
Behavioural models and parametrised systemsMeTRiD at S510
Chair(s): Tiziana Margaria University of Limerick and Lero - The Irish Software Research Centre
11:00
40m
Talk
Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries
MeTRiD
Nathalie Bertrand INRIA Rennes, Igor Konnov Inria Nancy, Marijana Lazić TU Wien, Josef Widder TU Wien
11:40
40m
Talk
Revisiting the Glue of BIP
MeTRiD
Jacques Combaz Verimag/CNRS
12:20
40m
Talk
Programming Dynamic Reconfigurable Systems with DR-BIP
MeTRiD
Rim El Ballouli Verimag, Saddek Bensalem Verimag, Marius Bozga Verimag/CNRS, Joseph Sifakis Verimag/CNRS
11:00 - 12:00
11:00
10m
Talk
Advances in Usability of Formal Methods for Code Verification
InterAVT
11:10
10m
Talk
Scalable Software Testing and Verification for Industrial-Scale Systems: The Challenges
InterAVT
Anila Mjeda Lero - The Irish Software Research Centre and University of Limerick, Goetz Botterweck Lero - The Irish Software Research Centre and University of Limerick
11:20
10m
Talk
AskTheCode: Interactive Call Graph Exploration for Error Fixing and Prevention
InterAVT
Robert Husak , Jan Kofroň Charles University, Filip Zavoral
11:30
30m
Talk
Lighting talks (non-authors)
InterAVT

11:00 - 12:30
ModellingHSB at S9
Chair(s): Tatjana Petrov Universität Konstanz
11:00
30m
Talk
A Hybrid HMM Approach for the Dynamics of DNA Methylation
HSB
Charalampos Kyriakopoulos Saarland University, Pascal Giehr Saarland University, Alexander Lück Saarland University, Jörn Walter Saarland University, Verena Wolf Saarland University
11:30
30m
Talk
Controlling noisy expression through auto regulation of burst frequency and protein stability
HSB
Pavol Bokes Comenius University, Abhyudai Singh University of Delaware
12:00
30m
Talk
Using a hybrid approach to model central carbon metabolism across the cell cycle
HSB
Cecile Moulin Laboratoire de Recherche en Informatique, Université Paris-Saclay & UMR CNRS 8623, Laurent Tournier MaIAGE, INRA, Université Paris-Saclay., Sabine Peres Laboratoire de Recherche en Informatique, Université Paris-Saclay & UMR CNRS 8623.
11:00 - 12:30
VerifyThis 2 (Verification challenge 1)TOOLympics at SU2
11:00 - 12:30
SV-COMP MeetingTOOLympics at SW2 (TOOLympics)
13:30 - 15:30
ApplicationsSynCoP at S10
13:45
45m
Talk
Parametric statistical model checking of UAV flightplan
SynCoP
14:30
45m
Talk
Fault-tolerant matrix factorisation: a formal model and proof
SynCoP
Camille Coti LIPN, Université Paris 13, Laure Petrucci Université Paris 13, Daniel Alberto Torres Gonzalez LIPN, Université Paris 13
13:30 - 15:30
IIIDICE-FOPARA at S11
Chair(s): Patrick Baillot CNRS & ENS Lyon
14:00
45m
Talk
Type-two Iteration with Bounded Query Revision
DICE-FOPARA
Bruce Kapron University of Victoria, Florian Steinberg INRIA Saclay
14:45
45m
Talk
Tiered complexity at higher order
DICE-FOPARA
Emmanuel Hainry , Bruce Kapron University of Victoria, Jean-Yves Marion LORIA, Romain Péchoux INRIA / LORIA
13:30 - 15:30
IIIGaLoP at S3
13:30
60m
Talk
Model checking games: the recent advances on parity games
GaLoP
I: Nathanaël Fijalkow CNRS, LaBRI, and Alan Turing Institute
14:30
30m
Talk
A Framework for Compositional Model Checking
GaLoP
Yu-Yang Lin Queen Mary University of London, Nikos Tzevelekos Queen Mary University of London
15:00
30m
Talk
Modalities as prices: a game model of intuitionistic linear logic with subexponentials
GaLoP
Timo Lang Vienna University of Technology, Chris Fermüller Vienna University of Technology, Elaine Pimentel Federal University of Rio Grande do Norte, Brazil, Carlos Olarte Federal University of Rio Grande do Norte, Brazil
13:30 - 15:30
Behavioural Types for API-based softwareBEHAPI at S4 (BEHAPI)
Chair(s): emilio tuosto University of Leicester
13:30
30m
Talk
Mailbox Types for Unordered Interactions
BEHAPI
Ugo de'Liguoro Università di Torino, Luca Padovani University of Turin
14:00
30m
Talk
A Behavioural Type System for Mungo with Generics
BEHAPI
A: Hans Hüttel Department of Computer Science, Aalborg University
14:30
30m
Talk
A Virtual-Machine Metaobject Protocol for Run-Time Software Adaptation
BEHAPI
Guido Chari Czech Technical University, Czechia
15:00
30m
Talk
Hardware Interactions as Behavioural Types.
BEHAPI
Francisco Martins University of Lisbon
13:30 - 15:30
IIIInterAVT at S6
13:30
2h
Meeting
Speed-dating
InterAVT

14:00 - 15:30
Afternoon AMooly Fest at JUPITER
14:00
30m
Talk
Proofs and Counterexamples
Mooly Fest
Neil Immerman University of Massachusetts, Amherst
14:30
30m
Talk
Concurrency Control Contract Composition
Mooly Fest
G. Ramalingam Microsoft Research
15:00
30m
Talk
Special Relations for Special Relationships
Mooly Fest
Nikolaj Bjørner Microsoft Research
14:00 - 15:30
RERS 1TOOLympics at S5
14:00 - 15:30
Keynote 2MeTRiD at S510
Chair(s): Panagiotis Katsaros ITI-CERTH, Thessaloniki
14:30
60m
Talk
Cyber-Physical Components as building blocks of more dependable industrial CPS
MeTRiD
Valeriy Vyatkin Aalto University, Finland and Luleå University of Technology, Sweden
14:00 - 15:30
Oded Maler memorial (1)HSB at S9
Chair(s): Nicola Paoletti Royal Holloway, University of London, UK
14:00
60m
Talk
Oded Maler: An odyssey from Computer Science to Biological Sciences
HSB
Thao Dang CNRS/VERIMAG
14:00 - 15:30
VerifyThis 3 (Verification challenge 3)TOOLympics at SU2
14:00 - 15:30
Test-Comp TalksTOOLympics at SW2 (TOOLympics)
16:00 - 18:00
16:00
30m
Talk
Automatic Equivalence Proofs for Programs with Algebraic Data Types
PERR
Moritz Kiefer , Mattias Ulbrich Karlsruhe Institute of Technology
16:30
30m
Talk
Proving Program Equivalence with Constrained Rewriting Induction and Ctrl
PERR
Carsten Fuhs Birkbeck, University of London, Cynthia Kop Radboud University Nijmegen, Naoki Nishida Nagoya University
17:00
30m
Talk
Semantics-Based Proofs of Equivalence for Functions with Accumulators
PERR
Stefan Ciobaca Alexandru Ioan Cuza University of Iasi, Dorel Lucanu , Sebastian Buruiana
16:00 - 18:00
BehAPI Business MeetingBEHAPI at S4 (BEHAPI)
Chair(s): Adrian Francalanza University of Malta
16:00
60m
Talk
BehAPI Practices
BEHAPI
Caroline Caruana University of Malta
17:00
60m
Meeting
BehAPI Year 1 Review and Year 2 projections
BEHAPI
Adrian Francalanza University of Malta
16:00 - 18:00
RERS 2TOOLympics at S5
16:00 - 18:00
Cyber-Physical Systems designMeTRiD at S510
Chair(s): Valeriy Vyatkin Aalto University, Finland and Luleå University of Technology, Sweden
16:00
40m
Talk
Localizing Faults in Simulink/Stateflow Models with STL
MeTRiD
Ezio Bartocci Technische Universität Wien, Thomas Ferrère IST Austria, Niveditha Manjunath Austrian Institute of Technology, Dejan Nickovic Austrian Institute of Technology
16:40
40m
Talk
Model-based energy characterization of IoT system design aspects
MeTRiD
Alexios Lekidis Aristotle University of Thessaloniki
17:20
40m
Talk
Modeling and Simulation of Attacks on Cyber-physical Systems
MeTRiD
Cinzia Bernardeshi Univ. of Pisa
16:00 - 18:00
16:00
75m
Meeting
Collaboration Session
InterAVT

17:15
15m
Talk
Wrap-up
InterAVT

16:00 - 18:00
Oded Maler memorial (2)HSB at S9
Chair(s): Nicola Paoletti Royal Holloway, University of London, UK
16:00
60m
Talk
From Sensitive to Formal Barbaric Systems Biology
HSB
Alexandre Donze University of California, Berkeley
17:00
60m
Talk
Timed Patterns: from Definition to Matching and Monitoring, a survey in memoriam Oded Maler
HSB
Eugene Asarin IRIF, University Paris Diderot and CNRS, France
16:00 - 18:00
VerifyThis 4 (Verification challenge 3)TOOLympics at SU2
16:00 - 18:00
Test-Comp MeetingTOOLympics at SW2 (TOOLympics)

Sun 7 Apr

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

08:00 - 09:00
Mentoring Breakfast IMentoring Workshop at JUPITER
09:00 - 10:30
Parameter synthesis for LTLSynCoP at S10
09:00
45m
Talk
Parameter Synthesis for Timed Automata with Clock-Aware LTL Properties
SynCoP
09:45
45m
Talk
Pruning NDFS for Parametric Timed Automata
SynCoP
Laure Petrucci Université Paris 13, Jaco van de Pol Aarhus University
09:00 - 10:30
VGaLoP at S3
09:00
60m
Talk
Template games: a homotopy model of differential linear logic
GaLoP
I: Paul-André Melliès CNRS and University Paris Diderot
10:00
30m
Talk
Simple game semantics and Day convolution
GaLoP
Clovis Eberhart National Institute of Informatics, Japan, Tom Hirschowitz Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry, Alexis Laouar Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS
09:00 - 10:30
09:00 - 10:30
Session 1PLACES at S8
Chair(s): Francisco Martins University of Lisbon
09:00
60m
Talk
Keynote: Unstructured Parallelism Considered Harmful -- Using Structured Parallelism for Enhanced Software Verification
PLACES
Vivek Sarkar Rice University, USA
10:00
30m
Full-paper
A Message-Passing Interpretation of Adjoint Logic
PLACES
Klaas Pruiksma Carnegie Mellon University, Frank Pfenning Carnegie Mellon University, USA
09:00 - 10:30
VHSB at S9
Chair(s): Nicola Paoletti Royal Holloway, University of London, UK
09:00
60m
Talk
Invited talk: Closed-loop neurohybrid interfaces: from in vitro to in vivo studies and beyond
HSB
Michela Chiappalone Italian Institute of Technology
10:00
30m
Talk
Temporal Logic Based Synthesis of Experimentally Constrained Interaction Networks
HSB
Judah Goldfeder Yeshiva University, Hillel Kugler Microsoft
09:00 - 10:30
VerifyThis 5 (Judging and team presentations 1)TOOLympics at SU2
09:00 - 10:30
Reactive Synthesis Background & SYNTCOMPSYNT Camp at SW2 (SYNT Camp)
Chair(s): Guillermo A. Perez University of Antwerp, Leander Tentrup Saarland University
09:00
60m
Tutorial
Reactive Synthesis Background and the Synthesis Competition
SYNT Camp
Guillermo A. Perez University of Antwerp
10:00
30m
Tutorial
Hand-on Synthesis Experience with BoSy
SYNT Camp
Leander Tentrup Saarland University
Link to publication DOI Pre-print
10:30 - 16:00
Workshop Poster Exhibition (Sunday)Posters at Coffee area (Posters)
10:30
22m
Poster
CPALockator: Thread-Modular Approach with Transition Abstraction for Analysis of Multithreaded Software
Posters
10:52
22m
Poster
CPAchecker with Strategy Selection
Posters
11:14
22m
Poster
CoVeriTest: Cooperative Verifier-Based Testing
Posters
Dirk Beyer LMU Munich, Marie-Christine Jakobs TU Darmstadt, Germany
11:36
22m
Poster
FreeST: context-free session types in a functional language
Posters
Bernardo Almeida Universidade de Lisboa, Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos University of Lisbon, Portugal
11:58
22m
Poster
JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)
Posters
Lucas Cordeiro University of Oxford, Daniel Kroening University of Oxford, Peter Schrammel University of Oxford, UK
12:20
22m
Poster
Markovian equivalences for biochemical reaction networks
Posters
Isabel Cristina Perez-Verona IMT Institute for Advanced Studies Lucca, Italy, Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy, Max Tschaikowski IMT Institute for Advanced Studies Lucca, Italy, Andrea Vandin DTU, Denmark, Luca Cardelli Microsoft Research and University of Oxford
12:42
22m
Poster
Minimal-Time Synthesis for Parametric Timed Automata
Posters
Étienne André LIPN, CNRS UMR 7030, Université Paris 13, Vincent Bloemen University of Twente, Laure Petrucci Université Paris 13, Jaco van de Pol Aarhus University
13:04
22m
Poster
PeSCo: Predicting Sequential Combinations of Verifiers
Posters
Pavel Andrianov , Heike Wehrheim Paderborn University
13:26
22m
Poster
Semantic Fault Localization and Suspiciousness Ranking
Posters
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
13:48
22m
Poster
Statistical abstraction for multi-scale spatio-temporal systems
Posters
Michalis Michaelides University of Edinburgh, Jane Hillston University of Edinburgh, Guido Sanguinetti University of Edinburgh
14:10
22m
Poster
Towards A Logical Account of Epistemic Causality
Posters
14:32
22m
Poster
Towards Efficient Algorithms for Constraint Satisfaction Problems
Posters
Huu-Phuc Vo Uppsala University
14:54
22m
Poster
Ultimate Automizer
Posters
Matthias Heizmann University of Freiburg, Yu-Fang Chen Academia Sinica, Daniel Dietsch University of Freiburg, Marius Greitschus , Jochen Hoenicke Universität Freiburg, Yong Li Institute of Software, Chinese Academy of Sciences, Alexander Nutz University of Freiburg, Germany, Pavel Andrianov , Christian Schilling IST Austria, Tanja Schindler University of Freiburg, Andreas Podelski University of Freiburg, Germany
15:16
22m
Poster
VIAP 1.1
Posters
15:38
22m
Poster
WAPS: Weighted and Projected Sampling
Posters
Rahul Gupta , Shubham Sharma , Subhajit Roy IIT Kanpur, India, Kuldeep S. Meel National University of Singapore
10:30 - 12:00
Morning Session IIMentoring Workshop at Mentoring
10:30
30m
Talk
How to Give an Effective Talk
Mentoring Workshop
Ajitha Rajan University of Edinburgh
11:00
30m
Talk
Navigating through the academic jungle: tips, tricks & traps
Mentoring Workshop
Marielle Stoelinga University of Twente and Radboud University, Nijmegen
11:30
30m
Talk
Push, Pull, Partner - A Few Models for Industrial Research
Mentoring Workshop
Thomas Ball Microsoft Research
11:00 - 12:00
11:00
60m
Talk
(Invited Talk) Cons-free Rewriting
DICE-FOPARA
Cynthia Kop Radboud University Nijmegen
11:00 - 12:00
VIGaLoP at S3
11:00
30m
Talk
A game semantics understanding of asynchronous multiparty session types subtyping
GaLoP
Simon Castellan , Alceste Scalas Aston University, Nobuko Yoshida Imperial College London
11:30
30m
Talk
Probabilistic Programming Inference via Intensional Semantics
GaLoP
Simon Castellan Imperial College London, UK, Hugo Paquet University of Cambridge
11:00 - 12:00
IIHCVS at S4 (HCVS)
Chair(s): Mattias Ulbrich Karlsruhe Institute of Technology
11:00
30m
Talk
Challenges in the specialisation of smart Horn clause interpreters
HCVS
John P. Gallagher Roskilde University
File Attached
11:30
30m
Full-paper
Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification
HCVS
Emanuele De Angelis University of Chieti-Pescara, Fabio Fioravanti University of Chieti-Pescara, Alberto Pettorossi University of Rome Tor Vergata, Italy, Maurizio Proietti CNR-IASI
File Attached
11:00 - 12:30
TOOLympics 1 - Pre-EventsTOOLympics at S5
11:00
11m
Meeting
CHC-COMP
TOOLympics

11:11
11m
Meeting
QComp
TOOLympics

11:22
11m
Meeting
Test-Comp
TOOLympics

11:33
11m
Meeting
SV-COMP
TOOLympics

11:45
11m
Meeting
RERS
TOOLympics

11:56
11m
Meeting
SAT
TOOLympics

12:07
11m
Meeting
SL-COMP
TOOLympics

12:18
11m
Meeting
TermCOMP
TOOLympics

11:00 - 12:30
11:00
30m
Invited Talk: Expected Cost Analysis of Attack-Defence Trees
SPIoT
Jan Kretinsky Technical University of Munich
11:30
30m
Talk
Static Analysis for the OWASP IoT Top 10 2018.
SPIoT
Pietro Ferrara JuliaSoft SRL, Italy, Amit Kr Mandal Università Ca' Foscari, Venezia, Italy, Agostino Cortesi Università Ca' Foscari Venezia, Fausto Spoto U. Verona
12:00
30m
Talk
The Refinement-Risk Loop - A Process for Security Engineering in Isabelle
SPIoT
Florian Kammüller Middlesex University, UK
11:00 - 12:00
IIPLACES at S8
Chair(s): Ornela Dardha University of Glasgow
11:00
30m
Full-paper
FreeST: context-free session types in a functional language
PLACES
Bernardo Almeida Universidade de Lisboa, Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos University of Lisbon, Portugal
11:30
30m
Full-paper
Concurrent Typestate-Oriented Programming in Java
PLACES
Rosita Gerbo Università di Torino, Luca Padovani University of Turin
11:00 - 12:30
AnalysisHSB at S9
Chair(s): Jerome Feret INRIA Paris
11:00
30m
Talk
Fixed-point Computation of Equilibria in Biochemical Regulatory Networks
HSB
Isabel Cristina Perez-Verona IMT Institute for Advanced Studies Lucca, Italy, Mirco Tribastone IMT Institute for Advanced Studies Lucca, Italy, Max Tschaikowski IMT Institute for Advanced Studies Lucca, Italy
11:30
30m
Talk
Rejection-Based Simulation of Stochastic Spreading Processes on Complex Networks
HSB
Gerrit Großmann Saarland University, Verena Wolf Saarland University
12:00
30m
Talk
rPrism -- A software for reactive weighted state transition models
HSB
Daniel Figueiredo University of Aveiro, Eugénio A. M. Rocha University of Aveiro, Madalena Chaves INRIA, Manuel A. Martins University of Aveiro
11:00 - 12:30
VerifyThis 6 (Judging and team presentations 2)TOOLympics at SU2
11:00 - 12:00
Hands-on BoSy TutorialSYNT Camp at SW2 (SYNT Camp)
Chair(s): Guillermo A. Perez University of Antwerp, Leander Tentrup Saarland University
11:00
60m
Tutorial
Hand-on Synthesis Experience with BoSy (part 2)
SYNT Camp
Leander Tentrup Saarland University
13:30 - 15:30
VIIDICE-FOPARA at S11
Chair(s): Marko van Eekelen Open University of the Netherlands
14:00
45m
Talk
Modular Runtime Complexity Analysis of Probabilistic While Programs
DICE-FOPARA
Martin Avanzini INRIA Sophia Antipolis, France, Michael Schaper University of Innsbruck, Georg Moser University of Innsbruck
14:45
45m
Talk
Type-Based Resource Analysis on Haskell
DICE-FOPARA
13:30 - 15:30
IIIHCVS at S4 (HCVS)
Chair(s): John P. Gallagher Roskilde University
13:30
60m
Invited Talk: Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts
HCVS
File Attached
14:30
30m
Talk
Coinduction in Uniform: what's next?
HCVS
Henning Basold CNRS & ENS Lyon, Ekaterina Komendantskaya Heriot-Watt University, UK
Link to publication
15:00
30m
Full-paper
Ultimate TreeAutomizer
HCVS
Daniel Dietsch University of Freiburg, Matthias Heizmann University of Freiburg, Jochen Hoenicke Universität Freiburg, Alexander Nutz University of Freiburg, Germany, Andreas Podelski University of Freiburg, Germany
13:30 - 15:30
IIIPLACES at S8
Chair(s): Vasco T. Vasconcelos University of Lisbon, Portugal
13:30
60m
Talk
Keynote: Shared Session Types for Safe, Practical Concurrency
PLACES
Stephanie Balzer Carnegie Mellon University
14:30
30m
Full-paper
Multiparty session type-safe web development with static linearity
PLACES
Jonathan King Habito and Imperial College London, Nicholas Ng Imperial College London, Nobuko Yoshida Imperial College London
15:00
30m
Full-paper
Service Equivalence via Multiparty Session Type Isomorphisms
PLACES
Assel Altayeva Imperial College London, Nobuko Yoshida Imperial College London
14:00 - 15:30
Afternoon Session IMentoring Workshop at Mentoring
14:00
30m
Talk
How to survive being a woman in computer science
Mentoring Workshop
Marieke Huisman University of Twente
14:30
30m
Talk
Advice on your adviser
Mentoring Workshop
Marsha Chechik University of Toronto
File Attached
15:00
30m
Talk
A few lessons from the PhD I just finished
Mentoring Workshop
Juliana Franco Microsoft Research, Cambridge
14:00 - 15:30
TOOLympics 2 - On-Site / PostTOOLympics at S5
14:00
11m
Meeting
CASC
TOOLympics

14:11
11m
Meeting
CoCo
TOOLympics

14:22
11m
Meeting
CRV
TOOLympics

14:33
11m
Meeting
SMT-COMP
TOOLympics

14:45
11m
Meeting
MCC
TOOLympics

14:56
11m
Meeting
REC
TOOLympics

15:07
11m
Meeting
Rodeo
TOOLympics

15:18
11m
Meeting
VerifyThis
TOOLympics

14:00 - 15:30
IISPIoT at S510
14:00
30m
Talk
ADTLang: A Programming Language Approach to Attack Defense Trees
SPIoT
René Rydhof Hansen Aalborg University, Denmark, Peter Gjøl Jensen Aalborg University, Denmark, Kim Larsen Aalborg University, Axel Legay INRIA Rennes, Danny Bøgsted Poulsen University of Kiel, Germany
14:30
30m
Talk
Learning from attacks and failures: generating reliability models from data
SPIoT
Marielle Stoelinga University of Twente and Radboud University, Nijmegen
15:00
30m
Talk
Graph-based Technique for Survivability Estimation and Optimization of IoT Applications
SPIoT
Vladimir Shakhov University of Ulsan, South Korea, Insoo Koo University of Ulsan, South Korea
14:00 - 15:30
Algebraic approaches to causalityCREST at S6
14:00
45m
Talk
Coalgebras for causality
CREST
Matteo Sammartino University College London
File Attached
14:45
45m
Talk
Causality and diagrammatic reasoning
CREST
14:00 - 15:30
VIIHSB at S9
Chair(s): David Safranek Masaryk University
14:00
60m
Talk
Invited talk: Reaction networks, stability of steady states, motifs for oscillatory dynamics, and parameter estimation in complex biochemical mechanisms
HSB
Igor Schreiber University of Chemistry and Technology of Prague
15:00
30m
Talk
Geometric fluid approximation for general continuous-time Markov chains
HSB
Michalis Michaelides University of Edinburgh, Jane Hillston University of Edinburgh, Guido Sanguinetti University of Edinburgh
16:00 - 18:00
VIIIGaLoP at S3
16:00 - 18:00
IVHCVS at S4 (HCVS)
Chair(s): Nikolaj Bjørner Microsoft Research
16:00
30m
Talk
Decomposing Farkas Interpolants
HCVS
Martin Blicha USI Lugano, Switzerland, Antti Hyvärinen , Jan Kofroň Charles University, Natasha Sharygina USI Lugano, Switzerland
File Attached
16:30
30m
Experience report
Report on the CHC competition
HCVS
Grigory Fedyukovich Princeton University
16:00 - 18:00
25 Years TACASTOOLympics at S5
16:00
2h
Meeting
Panel Discussion: Moore's Law, and More? (TACAS 25th anniversary)
TOOLympics
P: Marieke Huisman University of Twente, P: Rance Cleaveland University of Maryland, P: Holger Hermanns Saarland University, P: Kim Larsen Aalborg University, M: Bernhard Steffen Technical University Dortmund, Hubert Garavel
16:00 - 18:00
Session IVQAPL at S7
16:00
30m
Talk
Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs
QAPL
Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja RWTH Aachen University, Thomas Noll RWTH Aachen University
DOI
16:30
30m
Talk
An Adequate Semantics for Hybrid While
QAPL
Sergey Goncharov FAU Erlangen-Nürnberg, Lehrstuhl 8, Renato Neves University of Minho & INESC TEC
17:00
30m
Talk
Recent Applications and Quantitative Aspects of Spatial Model Checking
QAPL
17:30
30m
Talk
Equational Characterization Metaresults for Bisimulation and Trace Semantics in ULTraS
QAPL
Marco Bernardo University of Urbino
16:00 - 18:00
IVPLACES at S8
Chair(s): Francisco Martins University of Lisbon
16:00
30m
Full-paper
Value-Dependent Session Design in a Dependently Typed Language
PLACES
Jan de Muijnck-Hughes University of Glasgow, Edwin Brady University of St. Andrews, UK, Wim Vanderbauwhede University of Glasgow
16:30
30m
Talk
Fluid Types: Statically Verified Distributed Protocols with Refinements
PLACES
Fangyi Zhou Imperial College London, Francisco Ferreira Imperial College London, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London
17:00
30m
Talk
The Cpi-calculus: a Model for Confidential Name Passing
PLACES
Ivan Prokić University of Novi Sad
17:30
5m
Day closing
Closing remarks
PLACES

16:00 - 18:00
Synthesis and InferenceHSB at S9
Chair(s): Michela Chiappalone Italian Institute of Technology
16:00
30m
Talk
Extracting landscape features from single particle trajectories
HSB
Ádám Halász West Virginia University, Ouri Maler West Virginia University, Jeremy S Edwards University of New Mexico
16:30
30m
Talk
Fuzzy Matching in Symbolic Systems Biology
HSB
Adrian Riesco Universidad Complutense de Madrid, Beatriz Santos-Buitrago Seoul National University, Merrill Knapp SRI International, Gustavo Santos-Garcia Universidad de Salamanca, Carolyn Talcott SRI International
17:00
30m
Talk
Data-informed parameter synthesis for population Markov chains
HSB
Matej Hajnal Masaryk University, Tatjana Petrov Universität Konstanz, David Safranek Masaryk University, Morgane Nouvian University of Konstanz
17:30
10m
Day closing
Closing
HSB

16:30 - 17:30
Afternoon Session IIMentoring Workshop at Mentoring
17:00
30m
Talk
Science and Sanity: how to do the former while retaining the later (Panel)
Mentoring Workshop
Stephanie Balzer Carnegie Mellon University, Barbora Buhnova Masaryk University, Juliana Franco Microsoft Research, Cambridge

Mon 8 Apr

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

07:30 - 08:30
Mentoring Breakfast IIMentoring Workshop at MERCURY
08:40 - 09:00
OpeningSocial at SUN I
08:40
20m
Social Event
Opening
Social
Joost-Pieter Katoen RWTH Aachen University, Jan Vitek Northeastern University and Czech Technical University, Jan Kofroň Charles University
09:00 - 10:00
ChechikKeynotes at SUN I
Chair(s): Joost-Pieter Katoen RWTH Aachen University
09:00
60m
Talk
Software Assurance in an Uncertain World
Keynotes
Marsha Chechik University of Toronto
Link to publication File Attached
10:30 - 12:30
Applied CategoriesFOSSACS at MOON
Chair(s): Alex Simpson University of Ljubljana
10:30
30m
Talk
Trees in Partial Higher Dimensional AutomataBest paper nomination
FOSSACS
Link to publication
11:00
30m
Talk
Rewriting Abstract Structures: Materialization Explained CategoricallyBest paper nomination
FOSSACS
Andrea Corradini , Tobias Heindel , Barbara König University of Duisburg-Essen, Dennis Nolte University of Duisburg-Essen, Arend Rensink University of Twente, The Netherlands
Link to publication
11:30
30m
Talk
Change Actions: Models of Generalised Differentiation
FOSSACS
Mario Alvarez-Picallo University of Oxford, C.-H. Luke Ong University of Oxford
Link to publication
12:00
30m
Talk
Causal Inference by String Diagram Surgery
FOSSACS
Aleks Kissinger Radboud University, Bart Jacobs Radboud University Nijmegen, Fabio Zanasi University College London
Link to publication
10:30 - 12:30
SAT and SMT ITACAS at SUN I
Chair(s): Lijun Zhang Chinese Academy of Sciences
10:30
30m
Talk
Decomposing Farkas Interpolants
TACAS
Martin Blicha USI Lugano, Switzerland, Antti Hyvärinen , Jan Kofroň Charles University, Natasha Sharygina USI Lugano, Switzerland
Link to publication
11:00
30m
Talk
Parallel SAT Simplification on GPU Architectures
TACAS
Muhammad Osama Eindhoven University of Technology, Anton Wijs Eindhoven University of Technology
Link to publication
11:30
30m
Talk
Encoding Redundancy for Satisfaction-Driven Clause LearningBest paper nomination
TACAS
Marijn Heule The University of Texas at Austin, Benjamin Kiesl CISPA Helmholtz Center for Information Security, Armin Biere Johannes Kepler University Linz
Link to publication
12:00
30m
Talk
WAPS: Weighted and Projected Sampling
TACAS
Rahul Gupta , Shubham Sharma , Subhajit Roy IIT Kanpur, India, Kuldeep S. Meel National University of Singapore
Link to publication
10:30 - 12:30
Program VerificationESOP at SUN II
Chair(s): Luís Caires NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
10:30
30m
Talk
Time Credits and Time Receipts in Iris
ESOP
Glen Mével , Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, François Pottier Inria, France
Link to publication
11:00
30m
Talk
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
ESOP
Guido Martínez CIFASIS-CONICET, Argentina, Danel Ahman University of Ljubljana, Victor Dumitrescu Nomadic Labs Paris, Nick Giannarakis Princeton University, Chris Hawblitzel Microsoft Research, Cătălin Hriţcu Inria Paris, Monal Narasimhamurthy University of Colorado, Boulder, Zoe Paraskevopoulou Princeton University, Clément Pit-Claudel MIT CSAIL, Jonathan Protzenko Microsoft Research, Redmond, Tahina Ramananandro Microsoft Research, n.n., Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research
Link to publication
11:30
30m
Talk
Semi-Automated Reasoning About Non-Determinism in C Expressions
ESOP
Dan Frumin Radboud University, Léon Gondelman LRI, Université Paris-Sud, Robbert Krebbers Delft University of Technology
Link to publication
12:00
30m
Talk
Fixing Incremental Computation: Derivatives of fixpoints, and the recursive semantics of Datalog
ESOP
Michael Peyton Jones IOHK, Mario Alvarez-Picallo University of Oxford, Alexander Eyers-Taylor Semmle, C.-H. Luke Ong University of Oxford
Link to publication
14:00 - 16:00
Categories and (Co)algebraFOSSACS at MOON
Chair(s): Sergey Goncharov FAU Erlangen-Nürnberg, Lehrstuhl 8
14:00
30m
Talk
Equational Axiomatization of Algebras wth Structure
FOSSACS
Link to publication
14:30
30m
Talk
Equational Theories and Monads from Polynomial Cayley Representations
FOSSACS
Maciej Piróg University of Wrocław, Piotr Polesiuk University of Wrocław, Filip Sieczkowski University of Wrocław
Link to publication
15:00
30m
Talk
Path category for free - Open morphisms from coalgebras with non-deterministic branching
FOSSACS
Thorsten Wißmann Friedrich-Alexander-Universität Erlangen, Jérémy Dubut , Shin-ya Katsumata National Institute of Informatics, Ichiro Hasuo National Institute of Informatics
Link to publication
15:30
30m
Talk
Coalgebra Learning via Duality
FOSSACS
Simone Barlocco , Clemens Kupke University of Strathclyde, Jurriaan Rot Radboud University Nijmegen
Link to publication
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
14:00 - 16:00
Language DesignESOP at SUN II
Chair(s): Atsushi Igarashi Kyoto University, Japan
14:00
30m
Talk
Codata in Action
ESOP
Paul Downen University of Oregon, USA, Zachary Sullivan , Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft, UK
Link to publication
14:30
30m
Talk
Composing bidirectional programs monadically
ESOP
Li-yao Xia University of Pennsylvania, Dominic Orchard University of Kent, UK, Meng Wang University of Bristol, UK
Link to publication
15:00
30m
Talk
Counters in Kappa: Semantics, Simulation, and Static Analysis
ESOP
Pierre Boutillier , Ioana Cristescu INRIA, France, Jerome Feret INRIA Paris
Link to publication
15:30
30m
Talk
One Step at a Time
ESOP
Kathleen Fisher Tufts University, Ferdinand Vesely Swansea University
Link to publication
16:30 - 18:00
TinelliTutorials at MOON
Chair(s): Fabrice Kordon Sorbonne University — LIP6
16:30
90m
Talk
An overview of Satisfiability Modulo Theories and its applications
Tutorials
Cesare Tinelli University of Iowa
Link to publication
16:30 - 18:00
SAT Solving and Theorem ProvingTACAS at SUN I
Chair(s): Armin Biere Johannes Kepler University Linz
16:30
30m
Talk
Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks
TACAS
Pengfei Gao , Hongyi Xie , Jun Zhang , Fu Song , Taolue Chen Birkbeck, University of London
Link to publication
17:00
30m
Talk
Incremental Analysis of Evolving Alloy Models
TACAS
Wenxi Wang The University of Texas at Austin, Texas, USA, Kaiyuan Wang Google, Inc., Milos Gligoric University of Texas at Austin, Sarfraz Khurshid University of Texas at Austin
Link to publication
17:30
30m
Talk
Extending a Brainiac Prover to Lambda-Free Higher-Order Logic
TACAS
Link to publication
17:00 - 18:00
17:00
60m
Talk
Do programming languages matter for correctness of code? A reproduction study
Mentoring Workshop
Jan Vitek Northeastern University and Czech Technical University
18:30 - 20:30
Welcome and Poster ReceptionSocial at 1st Floor Reception Area
18:30 - 20:30
Main Poster SessionPosters at 1st Floor Reception Area (Posters)
Chair(s): Konrad Siek Czech Technical University in Prague
18:30
3m
Poster
Partial and Conditional Expectations in Markov Decision Processes with Integer Weights
Posters
Jakob Piribauer , Christel Baier TU Dresden, Germany
18:33
3m
Poster
Information Flow Control Parallel Runtime Systems Foundations
Posters
Marco Vassena Chalmers University of Technology, Deian Stefan University of California San Diego
18:37
3m
Poster
VyPR2: A Framework for Runtime Verification of Python Web Services
Posters
Joshua Dawes University of Manchester and CERN, Giles Reger University of Manchester, Giovanni Franzoni , Andreas Pfeiffer , Giacomo Govi
18:40
3m
Poster
Distributed Ledger Choreography Management via Provenance and Multiparty Session Type Isomorphisms
Posters
Assel Altayeva Imperial College London, Nobuko Yoshida Imperial College London
18:44
3m
Poster
Tool Support for Correctness-by-Construction
Posters
Tobias Runge TU Braunschweig, Thomas Thüm University of Ulm, Loek Cleophas Eindhoven University of Technology (TU/e) and Stellenbosch University (SU), Ina Schaefer Technische Universität Braunschweig, Bruce W Watson , Derrick Kourie Stellenbosch University
18:47
3m
Poster
Verifiably Safe Off-Model Reinforcement Learning
Posters
Nathan Fulton MIT-IBM Watson AI Lab, André Platzer Carnegie Mellon University
18:51
3m
Poster
Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware Approach
Posters
18:54
3m
Poster
FreeST: context-free session types in a functional language
Posters
Bernardo Almeida Universidade de Lisboa, Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos University of Lisbon, Portugal
18:58
3m
Poster
WAPS: Weighted and Projected Sampling
Posters
Rahul Gupta , Shubham Sharma , Subhajit Roy IIT Kanpur, India, Kuldeep S. Meel National University of Singapore
19:01
3m
Poster
Semantic Fault Localization and Suspiciousness Ranking
Posters
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
19:05
3m
Poster
The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and Usability
Posters
19:08
3m
Poster
Distributive Disjoint Polymorphism for Compositional Programming
Posters
Xuan Bi Standard Chartered Bank, Ningning Xie The University of Hong Kong, Bruno C. d. S. Oliveira The University of Hong Kong, Hong Kong, Tom Schrijvers KU Leuven
19:12
3m
Poster
Ultimate Automizer
Posters
Matthias Heizmann University of Freiburg, Yu-Fang Chen Academia Sinica, Daniel Dietsch University of Freiburg, Marius Greitschus , Jochen Hoenicke Universität Freiburg, Yong Li Institute of Software, Chinese Academy of Sciences, Alexander Nutz University of Freiburg, Germany, Pavel Andrianov , Christian Schilling IST Austria, Tanja Schindler University of Freiburg, Andreas Podelski University of Freiburg, Germany
19:15
3m
Poster
Automatically Identifying Sufficient Object Builders from Module APIs
Posters
Pablo Ponzio Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Valeria Bengolea Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Mariano Politano , Nazareno Aguirre Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Marcelo F. Frias Dept. of Software Engineering Instituto Tecnológico de Buenos Aires
19:19
3m
Poster
CPAchecker with Strategy Selection
Posters
19:22
3m
Poster
DeepFault: Fault Localization for Deep Neural Networks
Posters
19:26
3m
Poster
PhASAR: An Inter-Procedural Static Analysis Framework for C/C++
Posters
Philipp Dominik Schubert Heinz Nixdorf Institut, Paderborn University, Ben Hermann University of Paderborn, Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM
19:30
3m
Poster
Credential Scanning powered by Symbolic Regex Matching
Posters
Margus Veanes Microsoft Research, Olli Saarikivi , Eric Xu Microsoft, USA, Tiki Wan , Arvind Ravi Microsoft Azure
19:33
3m
Poster
ROLL 1.0: $\omega$-Regular Language Learning Library
Posters
Yong Li Institute of Software, Chinese Academy of Sciences, Xuechao Sun , Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Yu-Fang Chen Academia Sinica, Junnan Xu
19:37
3m
Poster
Parallel SAT Simplification on GPU Architectures
Posters
Muhammad Osama Eindhoven University of Technology, Anton Wijs Eindhoven University of Technology
19:40
3m
Poster
Computing Coupled Similarity
Posters
Benjamin Bisping Technische Universität Berlin, Uwe Nestmann
19:44
3m
Poster
Implementing SOS with Active Objects: A Case Study of a Multicore Memory System
Posters
Nikolaos Bezirgiannis , Frank S. de Boer Centrum Wiskunde & Informatica, Leiden University, Einar Broch Johnsen University of Oslo, Violet Ka I Pun , Silvia Lizeth Tapia Tarifa University of Oslo
19:47
3m
Poster
Minimal-Time Synthesis for Parametric Timed Automata
Posters
Étienne André LIPN, CNRS UMR 7030, Université Paris 13, Vincent Bloemen University of Twente, Laure Petrucci Université Paris 13, Jaco van de Pol Aarhus University
19:51
3m
Poster
PeSCo: Predicting Sequential Combinations of Verifiers
Posters
Pavel Andrianov , Heike Wehrheim Paderborn University
19:54
3m
Poster
The COMPASS 3.0 Toolset
Posters
Marco Bozzano , Harold Bruintjes , Alessandro Cimatti Fondazione Bruno Kessler, Joost-Pieter Katoen RWTH Aachen University, Thomas Noll RWTH Aachen University, Stefano Tonetta Fondazione Bruno Kessler, Italy
19:58
3m
Poster
CoVeriTest: Cooperative Verifier-Based Testing
Posters
Dirk Beyer LMU Munich, Marie-Christine Jakobs TU Darmstadt, Germany
20:01
3m
Poster
Decomposing Farkas Interpolants
Posters
Martin Blicha USI Lugano, Switzerland, Antti Hyvärinen , Jan Kofroň Charles University, Natasha Sharygina USI Lugano, Switzerland
20:05
3m
Poster
ILAng: A Modeling and Verification Platform for SoCs using Instruction-Level Abstractions
Posters
Bo-Yuan Huang Princeton University, USA, Hongce Zhang , Aarti Gupta Princeton University, Sharad Malik Princeton University
20:08
3m
Poster
JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)
Posters
Lucas Cordeiro University of Oxford, Daniel Kroening University of Oxford, Peter Schrammel University of Oxford, UK
20:12
3m
Poster
CLTestCheck: Measuring Test Effectiveness for GPU Kernels
Posters
Chao Peng University of Edinburgh, UK, Ajitha Rajan University of Edinburgh
20:15
3m
Poster
Business Process Privacy Analysis in Pleak
Posters
20:19
3m
Poster
Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking
Posters
Ilina Stoilkovska Vienna University of Technology , Igor Konnov Inria Nancy, Josef Widder TU Wien, Florian Zuleger Vienna University of Technology
20:22
3m
Poster
CPALockator: Thread-Modular Approach with Transition Abstraction for Analysis of Multithreaded Software
Posters
20:26
3m
Poster
Constraint-based Monitoring of Hyperproperties
Posters

Tue 9 Apr

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

08:00 - 09:00
Mentoring Breakfast IIIMentoring Workshop at MERCURY
09:00 - 10:00
ColcombetKeynotes at SUN I
Chair(s): Mikolaj Bojanczyk University of Warsaw
09:00
60m
Talk
On infinite duration games
Keynotes
Thomas Colcombet IRIF, University Paris Diderot and CNRS, France
Link to publication File Attached
10:30 - 12:30
Software Verification IFASE at JUPITER
Chair(s): Wil van der Aalst RWTH Aachen
10:30
30m
Talk
Tool Support for Correctness-by-Construction
FASE
Tobias Runge TU Braunschweig, Ina Schaefer Technische Universität Braunschweig, Loek Cleophas Eindhoven University of Technology (TU/e) and Stellenbosch University (SU), Thomas Thüm University of Ulm, Derrick Kourie Stellenbosch University, Bruce W Watson
Link to publication
11:00
30m
Talk
Automatic Modeling for Opaque Code in JavaScript Static Analysis
FASE
Joonyoung Park , Alexander Jordan Oracle Labs, Australia, Sukyoung Ryu KAIST, South Korea
Link to publication
11:30
30m
Talk
SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language
FASE
Min Zhang East China Normal University, Fu Song , Frederic Mallet Université Côte d'Azur, France, Xiaohong Chen
Link to publication
12:00
30m
Talk
A Hybrid Dynamic Logic for Event/Data-based SystemsBest paper nomination
FASE
Rolf Hennicker Ludwig Maximilians University Munich, Germany, Alexandre Madeira , Alexander Knapp
Link to publication
10:30 - 12:30
TypesESOP at SUN II
Chair(s): Vasco T. Vasconcelos University of Lisbon, Portugal
10:30
30m
Talk
Handling polymorphic algebraic effects
ESOP
Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan
Link to publication
11:00
30m
Talk
Distributive Disjoint Polymorphism for Compositional Programming
ESOP
Xuan Bi Standard Chartered Bank, Ningning Xie The University of Hong Kong, Bruno C. d. S. Oliveira The University of Hong Kong, Hong Kong, Tom Schrijvers KU Leuven
Link to publication
11:30
30m
Talk
Types by Need
ESOP
Beniamino Accattoli Inria & Ecole Polytechnique, Giulio Guerrieri University of Bath, Maico Leberle
Link to publication
12:00
30m
Talk
Verifiable certificates for predicate subtyping
ESOP
Link to publication
14:00 - 15:00
Machine LearningTACAS at JUPITER
Chair(s): Bernhard Steffen Technical University Dortmund
14:00
30m
Talk
Omega-Regular Objectives in Model-Free Reinforcement Learning
TACAS
Ernst Moritz Hahn Queen's University Belfast, Mateo Perez , Sven Schewe University of Liverpool, Fabio Somenzi , Ashutosh Trivedi , Dominik Wojtczak
Link to publication
14:30
30m
Talk
Verifiably Safe Off-Model Reinforcement Learning
TACAS
Nathan Fulton MIT-IBM Watson AI Lab, André Platzer Carnegie Mellon University
Link to publication
14:00 - 16:00
Tool DemosTACAS at SUN I
Chair(s): Marius Mikucionis Aalborg University
14:00
15m
Talk
nonreach – A Tool for Nonreachability Analysis
TACAS
Florian Messner , Christian Sternagel University of Innsbruck, Austria
Link to publication
14:15
15m
Talk
The Quantitative Verification Benchmark Set
TACAS
Arnd Hartmanns University of Twente, Michaela Klauck Saarland Informatics Campus, Saarland University, David Parker University of Birmingham, Tim Quatmann RWTH Aachen University, Enno Ruijters
Link to publication
14:30
15m
Talk
ILAng: A Modeling Platform for SoC Verification using Instruction-Level Abstractions
TACAS
Bo-Yuan Huang Princeton University, USA, Hongce Zhang , Aarti Gupta Princeton University, Sharad Malik Princeton University
Link to publication
14:45
15m
Talk
MetAcsl: Specification and Verification of High-Level Properties
TACAS
Link to publication
15:00
15m
Talk
ROLL 1.0: $\omega$-Regular Language Learning Library
TACAS
Yu-Fang Chen Academia Sinica, Yong Li Institute of Software, Chinese Academy of Sciences, Xuechao Sun , Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Junnan Xu
Link to publication
15:15
15m
Talk
Symbolic Regex Matcher
TACAS
Margus Veanes Microsoft Research, Olli Saarikivi , Eric Xu Microsoft, USA, Tiki Wan
Link to publication
15:30
15m
Talk
COMPASS 3.0
TACAS
Marco Bozzano , Harold Bruintjes , Alessandro Cimatti Fondazione Bruno Kessler, Joost-Pieter Katoen RWTH Aachen University, Thomas Noll RWTH Aachen University, Stefano Tonetta Fondazione Bruno Kessler, Italy
Link to publication
15:45
15m
Talk
Debugging of Behavioural Models with CLEAR
TACAS
Gianluca Barbon Universit� Grenoble Alpes, Inria, LIG, Vincent Leroy University of Grenoble - CNRS, Gwen Salaün University of Grenoble Alpes
Link to publication
14:00 - 16:00
Program SemanticsESOP at SUN II
Chair(s): Andrzej Murawski University of Oxford
14:00
30m
Talk
Extended call-by-push-value: reasoning about effectful programs and evaluation orderBest paper nomination
ESOP
Dylan McDermott University of Cambridge, Alan Mycroft University of Cambridge
Link to publication
14:30
30m
Talk
Effectful Normal-Form Bisimulation
ESOP
Ugo Dal Lago University of Bologna / Inria, Francesco Gavazzo
Link to publication
15:00
30m
Talk
On the Multi-Language Construction
ESOP
Samuele Buro Università degli Studi di Verona, Isabella Mastroeni University of Verona, Italy
Link to publication
15:30
30m
Talk
Probabilistic Programming Inference via Intensional Semantics
ESOP
Simon Castellan Imperial College London, UK, Hugo Paquet University of Cambridge
Link to publication
16:30 - 18:00
BeyerTutorials at SUN II
Chair(s): Joost-Pieter Katoen RWTH Aachen University
16:30
90m
Talk
Software Verification — An Overview of the State of the Art
Tutorials
Dirk Beyer LMU Munich
File Attached
17:00 - 18:00
17:00
60m
Talk
A tale of two MURIs: Authorization Meets Model Checking
Mentoring Workshop
Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc.
18:00 - 20:00
ETAPS SC MeetingSocial at MOON
18:00
2h
Meeting
ETAPS Steering committee meeting
Social
Joost-Pieter Katoen RWTH Aachen University, Holger Hermanns Saarland University, Gilles Barthe IMDEA Software Institute, Gerald Lüttgen University of Bamberg, Tarmo Uustalu Reykjavik University, Vladimiro Sassone University of Southampton, Lenore Zuck University of Illinois at Chicago, Luís Caires NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa, Peter Müller ETH Zurich, Peter Thiemann University of Freiburg, Germany, Reiner Hähnle Technical University of Darmstadt, Wil van der Aalst RWTH Aachen, Heike Wehrheim Paderborn University, Jordi Cabot ICREA - UOC, Gabriele Taentzer Universität Marburg, Mikolaj Bojanczyk University of Warsaw, Alex Simpson University of Ljubljana, Barbara König University of Duisburg-Essen, Andrew M. Pitts University of Cambridge, Flemming Nielson Technical University of Denmark, Dave Sands Chalmers, Matteo Maffei TU Wien, Tomáš Vojnar Brno University of Technology, Lijun Zhang Chinese Academy of Sciences, Armin Biere Johannes Kepler University Linz, David Parker University of Birmingham, Kim Larsen Aalborg University, Panagiotis Katsaros ITI-CERTH, Thessaloniki, Jan Vitek Northeastern University and Czech Technical University, Jan Kofroň Charles University, Tiziana Margaria University of Limerick and Lero - The Irish Software Research Centre , Anton Wijs Eindhoven University of Technology, Jurriaan Hage Utrecht University, Reiko Heckel University of Leicester, Catuscia Palamidessi INRIA and LIX, Don Sannella University of Edinburgh

Wed 10 Apr

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

08:00 - 09:00
Mentoring Breakfast IVMentoring Workshop at MERCURY
09:00 - 10:00
FisherKeynotes at SUN I
Chair(s): Luís Caires NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
09:00
60m
Talk
From quadcopters to helicopters: Formal verification to eliminate exploitable bugs
Keynotes
Kathleen Fisher Tufts University
File Attached
10:30 - 12:30
Security and Incremental ComputationESOP at SUN II
Chair(s): Zhong Shao Yale University
10:30
30m
Talk
Robustly Safe Compilation
ESOP
Marco Patrignani Stanford University & CISPA Helmholtz Center for Information Security, Deepak Garg Max Planck Institute for Software Systems
Link to publication
11:00
30m
Talk
Compiling Sandboxes: Formally Verified Software Fault Isolation
ESOP
Frédéric Besson , Sandrine Blazy Univ Rennes- IRISA, Alexandre Dang , Thomas P. Jensen INRIA Rennes, Pierre Wilke Yale University
Link to publication
11:30
30m
Talk
Safe Deferred Memory Reclamation with Types
ESOP
Ismail Kuru Drexel University, Colin Gordon Drexel University
Link to publication
12:00
30m
Talk
Incremental λ-Calculus in Cache-Transfer Style, Static Memoization by Program Transformation
ESOP
Paolo G. Giarrusso TU Delft, The Netherlands, Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Philipp Schuster University of Tübingen, Germany
Link to publication
13:00 - 14:00
General AssemblySocial at SUN II
13:00
60m
Meeting
ETAPS eV General Assembly
Social

14:00 - 16:00
Concurrency and DistributionESOP at SUN II
Chair(s): Luca Padovani University of Turin
14:00
30m
Talk
Asynchronous timed session types: duality and time-sensitive processes
ESOP
Laura Bocchi University of Kent, Maurizio Murgia , Vasco T. Vasconcelos University of Lisbon, Portugal, Nobuko Yoshida Imperial College London
Link to publication
14:30
30m
Talk
Manifest Deadlock-Freedom for Shared Session Types
ESOP
Stephanie Balzer Carnegie Mellon University, Bernardo Toninho Imperial College London, Frank Pfenning Carnegie Mellon University, USA
Link to publication
15:00
30m
Talk
A Categorical Model of an i/o-typed pi-calculus
ESOP
Ken Sakayori The University of Tokyo, Takeshi Tsukada University of Tokyo, Japan
Link to publication
15:30
30m
Talk
A Process Algebra for Link Layer Protocols
ESOP
Link to publication
17:00 - 18:00
17:00
60m
Talk
Formal methods can be practical: Verifying time-critical systems
Mentoring Workshop
Reinhard Wilhelm Saarland University
19:30 - 23:00
19:30
3h30m
Social Event
Banquet
Social
Jan Kofroň Charles University

Thu 11 Apr

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

09:00 - 10:00
FlanaganKeynotes at SUN I
Chair(s): Tomáš Vojnar Brno University of Technology
09:00
60m
Talk
Towards Efficient and Precise Concurrent Software Analysis
Keynotes
Cormac Flanagan University of California, Santa Cruz
File Attached
10:30 - 12:30
Covert Channels and Information FlowPOST at MOON
10:30
30m
Talk
Foundations for Parallel Information Flow Control Runtime Systems
POST
Marco Vassena Chalmers University of Technology, Gary Soeller , Peter Amidon , Matthew Chan , John Renner University of California, San Diego, Deian Stefan University of California San Diego
Link to publication
11:00
30m
Talk
A Formal Analysis of Timing Channel Security via Bucketing
POST
Tachio Terauchi Waseda University, Timos Antonopoulos Yale University
Link to publication
11:30
30m
Talk
A Dependently Typed Library for Static Information-Flow Control in Idris
POST
Simon Oddershede Gregersen Aarhus University, Søren Eller Thomsen Aarhus University, Aslan Askarov Aarhus University
Link to publication
12:00
30m
Talk
Achieving Safety Incrementally with Checked C
POST
Andrew Ruef , Leonidas Lampropoulos University of Pennsylvania, Ian Sweet , David Tarditi , Michael Hicks University of Maryland, College Park
Link to publication
10:30 - 12:30
Program Analysis and Automated VerificationESOP at SUN II
Chair(s): Stephanie Balzer Carnegie Mellon University
10:30
30m
Talk
Data-Races and Static Analysis for Interrupt-Driven Kernels
ESOP
Link to publication
11:00
30m
Talk
An abstract domain for trees with numeric relations
ESOP
Matthieu Journault , Antoine Miné UPMC, France, Abdelraouf Ouadjaout Sorbonne Université
Link to publication
11:30
30m
Talk
A static higher-order dependency pair framework
ESOP
Carsten Fuhs Birkbeck, University of London, Cynthia Kop Radboud University Nijmegen
Link to publication
12:00
30m
Talk
Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses
ESOP
Henning Basold CNRS & ENS Lyon, Ekaterina Komendantskaya Heriot-Watt University, UK, Yue Li Heriot-Watt University, UK
Link to publication
14:00 - 16:00
Specification, Design, and Implementation of Particular Classes of SystemsFASE at JUPITER
Chair(s): Reiner Hähnle Technical University of Darmstadt
14:00
30m
Talk
CLTestCheck: Measuring Test Effectiveness for GPU Kernels
FASE
Chao Peng University of Edinburgh, UK, Ajitha Rajan University of Edinburgh
Link to publication
14:30
30m
Talk
Implementing SOS with Active Objects: A Case Study of a Multicore Memory System
FASE
Nikolaos Bezirgiannis , Frank S. de Boer Centrum Wiskunde & Informatica, Leiden University, Einar Broch Johnsen University of Oslo, Violet Ka I Pun , Silvia Lizeth Tapia Tarifa University of Oslo
Link to publication
15:00
30m
Talk
Optimal and Automated Deployment for Microservices
FASE
Mario Bravetti Università di Bologna, Saverio Giallorenzo Alma Mater Studiorum - Università di Bologna, Jacopo Mauro University of Southern Denmark, Iacopo Talevi , Gianluigi Zavattaro
Link to publication
15:30
30m
Talk
A Data Flow Model with Frequency Arithmetic
FASE
Link to publication
14:00 - 16:00
Safety and Fault-tolerant SystemsTACAS at SUN I
Chair(s): Rance Cleaveland University of Maryland
14:00
30m
Talk
Digital Bifurcation Analysis of TCP Dynamics
TACAS
Link to publication
14:30
30m
Talk
Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking
TACAS
Ilina Stoilkovska Vienna University of Technology , Igor Konnov Inria Nancy, Josef Widder TU Wien, Florian Zuleger Vienna University of Technology
Link to publication
15:00
30m
Talk
Measuring Masking Fault-Tolerance
TACAS
Pablo Castro Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Pedro D'Argenio , Ramiro Demasi , Luciano Putruele
Link to publication
15:30
30m
Talk
PhASAR: An Inter-Procedural Static Analysis Framework for C/C++
TACAS
Philipp Dominik Schubert Heinz Nixdorf Institut, Paderborn University, Ben Hermann University of Paderborn, Eric Bodden Heinz Nixdorf Institut, Paderborn University and Fraunhofer IEM
Link to publication
16:30 - 18:00
Software TestingFASE at JUPITER
Chair(s): Silvia Lizeth Tapia Tarifa University of Oslo
16:30
30m
Talk
CoVeriTest: Cooperative, Verifier-Based Testing
FASE
Dirk Beyer LMU Munich, Marie-Christine Jakobs TU Darmstadt, Germany
Link to publication
17:00
30m
Talk
Pardis: Priority Aware Test Case Reduction
FASE
Golnaz Gharachorlu , Nick Sumner Simon Fraser University
Link to publication
17:30
30m
Talk
Automatically Identifying Sufficient Object Builders from Module APIs
FASE
Pablo Ponzio Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Valeria Bengolea Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Mariano Politano , Nazareno Aguirre Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Marcelo F. Frias Dept. of Software Engineering Instituto Tecnológico de Buenos Aires
Link to publication
16:30 - 17:00
Verification (continued)FOSSACS at SUN II
Chair(s): Mikolaj Bojanczyk University of Warsaw
16:30
30m
Talk
The Bernays-Schoenfinkel-Ramsey Class of Separation Logic on Arbitrary DomainsBest paper nomination
FOSSACS
Mnacho Echenim , Radu Iosif VERIMAG, CNRS, Université Grenoble-Alpes, Nicolas Peltier
Link to publication