Program - ETAPS 2019

ETAPS 2019 (series) /

ETAPS 2019 Program

Detailed Table Session Timeline Detailed Timeline

Switch Program View

You're viewing a filtered program.

Do you want to keep these filters active in the new view?

Get Calendar (iCal)

Filter Program | active: HSB

Dates

Nothing to filter

Rooms

1st Floor Reception Area

1st Floor Reception Area (Coffee)

1st Floor Reception Area (Posters)

Břevnovský klášter

Coffee area (Posters)

JUPITER

MERCURY

MOON

Mentoring

S1 (PERR)

S10

S11

S4 (BEHAPI)

S4 (HCVS)

S510

SU2

SUN I

SUN II

SW2 (SYNT Camp)

SW2 (TOOLympics)

HSB

Tracks

Nothing to filter

Badges

Nothing to filter

Your Program

Nothing to filter

Program Display Configuration

Time Zone

The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

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:00	Morning AMooly Fest at JUPITER

09:00 30m Talk		Calculational design of a static dependency analysis Mooly Fest Patrick Cousot
09:30 30m Talk		Automatic Detection of all Smart Contract Bugs Mooly Fest Mooly Sagiv Tel Aviv University

09:00 - 10:30	IPERR at S1 (PERR)

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 Luc Pellissier , Thomas Seiller CNRS

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	IInterAVT at S6

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 Iulia Dragomir , Saddek Bensalem Verimag

09:00 - 10:30	LiVe at S7

09:00 5m Talk		Opening LiVe
09:05 55m Talk		Invited talk: Bettina Könighofer: Safe and Optimized Learning via Shielding LiVe
10:00 30m Talk		Industrial talk: Martin Neuhäußer (Siemens): Verifying the approximate: Challenges in neural network analysis LiVe

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	SV-COMP TalksTOOLympics at SW2 (TOOLympics)

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 pritom rajkhowa , Fangzhen Lin
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 Karlheinz Friedberger , Marie-Christine Jakobs TU Darmstadt, Germany, Thomas Lemberger , Martin Spiessl , Philipp Wendler
13:48 22m Poster		Towards A Logical Account of Epistemic Causality Posters Shakil Khan , Mikhail Soutchanski
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 Pavel Andrianov , Pavel Andrianov , Pavel Andrianov

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:30	IIPERR at S1 (PERR)

11:00 30m Talk		Understanding Counterexamples for Relational Properties with DIbugger PERR Mihai Herda , Michael Kirsten Karlsruhe Institute of Technology (KIT), Etienne Brunner , Joana Plewnia , Ulla Scheler , Chiara Staudenmaier , Benedikt Wagner , Pascal Zwick , Bernhard Beckert Karlsruhe Institute of Technology
11:30 30m Talk		Analysis of program differences with numerical abstract interpretation PERR David Delmas Airbus & Sorbonne Université, Antoine Miné UPMC, France Link to publication Pre-print File Attached
12:00 30m Talk		On Quantitative Comparison of Chemical Reaction Network Models PERR Ozan Kahramanogullari

11:00 - 12:00	Timed systemsSynCoP at S10

11:00 45m Talk		On Parameterised Jobshop Scheduling Problems SynCoP Peter Habermehl IRIF

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 Damiano Mazza CNRS

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	IIInterAVT at S6

11:00 10m Talk		Advances in Usability of Formal Methods for Code Verification InterAVT Andre Maroneze , Valentin Perrelle , Florent Kirchner
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:00	LiVe at S7

11:00 15m Talk		Industrial talk: Vahid Hashemi (AUDI): Industrial View on Safety of Learning LiVe
11:15 15m Talk		Marielle Stoelinga: Learning from failures: generating reliability models from data LiVe
11:30 15m Talk		Nathanaël Fijalkow: Data generation for programming by example LiVe
11:45 15m Talk		Nils Jansen: Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks LiVe

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 Ran Bao , Christian Attiogbe , Benoit Delahaye
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

13:30 - 15:30	LiVe at S7

13:30 60m Talk		Invited talk: Kristian Kersting: Exploiting Symmetries for Modelling and Solving Quadratic Programs LiVe
14:30 60m Talk		Daniel Neider: Horn-ICE Learning LiVe

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	IIIPERR at S1 (PERR)

14:00 60m Talk		Invited talk by Marco Eilers PERR Marco Eilers ETH Zurich
15:00 30m Talk		Relational Verification via Invariant-Guided Synchronization PERR Qi Zhou , David Heath , William Harris

	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 - 17:00	Afternoon BMooly Fest at JUPITER

16:00 30m Talk		Decidable Reasoning for Verification: How Far Can You EPR? Mooly Fest Oded Padon Stanford University
16:30 30m Talk		code2seq: Generating Sequences from Structured Representations of Code Mooly Fest Eran Yahav Technion

16:00 - 18:00	IVPERR at S1 (PERR)

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 Ștefan Ciobâcă Alexandru Ioan Cuza University of Iasi, Dorel Lucanu , Sebastian Buruiana

16:00 - 18:00	Markov decision processesSynCoP at S10

16:00 45m Talk		Convex Optimization meets Parameter Synthesis for MDPs SynCoP Nils Jansen
16:45 45m Talk		Learning-Based Mean-Payoff Optimization in an unknown MDP under Omega-Regular Constraints SynCoP Jan Kretinsky Technical University of Munich

16:00 - 18:00	IVDICE-FOPARA at S11 Chair(s): Damiano Mazza CNRS

16:00 45m Talk		Pointers in Recursion: Exploring the Tropics DICE-FOPARA Paulin Jacobé De Naurois
16:45 45m Talk		Hierarchical Digging is EXPTIME DICE-FOPARA Brian Redmond

16:00 - 18:00	IVGaLoP at S3

16:00 30m Talk		Sequential algorithms and innocent strategies share the same execution mechanism GaLoP Pierre-Louis Curien Univ. Paris Diderot and INRIA Paris-Rocquencourt
16:30 40m Talk		A Dialectica-Like Interpretation of a Linear MSO on Infinite Words GaLoP Colin Riba , Pierre Pradic

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	IVInterAVT at S6

16:00 75m Meeting		Collaboration Session InterAVT
17:15 15m Talk		Wrap-up InterAVT

16:00 - 18:00	LiVe at S7

16:00 20m Talk		Stefan Ratschan: Learning Certificates LiVe
16:20 20m Talk		Yutaka Nagashima: Towards Machine Learning Induction LiVe
16:40 20m Talk		Maximilian Weininger: BRTDP for Stochastic Games LiVe

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:00	Morning Session IMentoring Workshop at Mentoring

09:00 60m Talk		From Shape Analysis to Smart Contract Verification: A journey in proof automationKeynote Mentoring Workshop Mooly Sagiv Tel Aviv University File Attached

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 Nikola Benes
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	VDICE-FOPARA at S11 Chair(s): Thomas Seiller CNRS

09:00 45m Talk		Finite semantics of polymorphism, complexity and the power of type fixpoints DICE-FOPARA Lê Thành Dũng Nguyễn , Thomas Seiller CNRS, Paolo Pistone University of Tübingen, Lorenzo Tortora de Falco
09:45 45m Talk		From normal functors to logarithmic space queries DICE-FOPARA Lê Thành Dũng Nguyễn , Pierre Pradic

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	IHCVS at S4 (HCVS) Chair(s): Maurizio Proietti CNR-IASI

09:00 60m		Invited Talk: Concolic testing of higher-order functional languages HCVS Konstantinos (Kostis) Sagonas Uppsala University File Attached
10:00 30m Talk		HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories HCVS C.-H. Luke Ong University of Oxford, Dominik Wagner Pre-print File Attached

	09:00 - 10:30	MCCTOOLympics at S5

09:00 - 10:30	Actual causationCREST at S6

09:00 45m Talk		Probabilistic Actual Causation CREST Luke Fenton-Glynn University College London File Attached
09:45 25m Research paper		Causality & Control flow [Robert Kunnemann, Deepak Garg, Michael Backes] CREST File Attached
10:10 20m Research paper		Extending Causal Models from Machines into Humans [Severin Kacianka, Amjad Ibrahim, Alexander Pretschner, Alexander Trende, Andreas Ludtke] CREST File Attached

09:00 - 10:30	Session IQAPL at S7

09:00 60m Talk		Principles of QAPL: What I learned in nearly 20 years and what I still don’t understand QAPL Herbert Wiklicky Imperial College London
10:00 30m Talk		Probabilistic output analyses for deterministic programs -reusing existing non-probabilistic analyses QAPL Maja Kirkeby Roskilde University Pre-print

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 Pavel Andrianov , Pavel Andrianov , Pavel Andrianov
10:52 22m Poster		CPAchecker with Strategy Selection Posters Karlheinz Friedberger , Marie-Christine Jakobs TU Darmstadt, Germany, Thomas Lemberger , Martin Spiessl , Philipp Wendler
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 Shakil Khan , Mikhail Soutchanski
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 pritom rajkhowa , Fangzhen Lin
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	SMTSynCoP at S10

11:00 45m Talk		SMT-based bounded model checking for parametric reaction systems SynCoP Wojciech Penczek IPI-PAN, Artur Meski

11:00 - 12:00	VIDICE-FOPARA at S11 Chair(s): Paulin Jacobé De Naurois

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	ISPIoT at S510

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:30	Causal discovery methodsCREST at S6

11:00 45m Talk		Computational Causal Discovery and its Applications CREST Sisi Ma University of Minnesota File Attached
11:45 45m Talk		Towards a Science of Perspicuous Computing - Lessons learnt from the Analysis of Automotive Emissions Control Systems CREST Holger Hermanns Saarland University File Attached

11:00 - 12:30	Session IIQAPL at S7

11:00 30m Talk		A Faster-Than Relation for Semi-Markov Decision Processes QAPL Mathias Ruggaard Pedersen Aalborg University, Giorgio Bacci Aalborg University, Kim Larsen Aalborg University Pre-print
11:30 30m Talk		Automatic Synthesis of Polynomial Probabilistic Invariants via Geometric Persistence QAPL Anne Schreuder Technischen Universität Kaiserslautern, C.-H. Luke Ong University of Oxford Pre-print
12:00 30m Talk		Towards Digital Twins for the Description of Automotive Software Systems QAPL Jan Olaf Blech Aalto University Pre-print

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	Stochastic systemsSynCoP at S10

13:30 45m Talk		Parametric Markov chains: algorithms, complexity and applications SynCoP Christel Baier TU Dresden, Germany
14:15 45m Talk		Parametric Verification and Synthesis based on Gaussian Processes SynCoP Simone Silvetti , Luca Bortolussi University of Trieste, Laura Nenzi

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 Franz Siglmüller

13:30 - 15:30	VIIGaLoP at S3

13:30 30m Talk		Full Abstraction for the Quantum Lambda-Calculus GaLoP Pierre Clairambault CNRS & ENS Lyon, Marc De Visme ENS Lyon
14:00 30m Talk		Some ideas for a finite geometry of interaction model of second-order MLL GaLoP Lê Thành Dũng Nguyễn
14:30 30m Talk		Bouncing Threads for Infinitary and Circular Proofs GaLoP David Baelde LSV, ENS Cachan, Amina Doumane , Denis Kuperberg , Alexis Saurin
15:00 30m Talk		Towards Circular Proof Nets GaLoP Abhishek De IRIF, CNRS, France, Alexis Saurin

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 Matteo Maffei TU Wien 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 Jean Krivine CNRS

14:00 - 15:30	Session IIIQAPL at S7

14:00 60m Talk		Invited talk: Exact and Approximate Reductions of Quantitative Models QAPL I: Max Tschaikowski TU Wien
15:00 30m Talk		Coherent Resolutions of Nondeterminism QAPL Marco Bernardo University of Urbino

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	VIII (cancelled)DICE-FOPARA at S11

16:00 45m Talk		Applications of Linear Defeasible Logic: combining resource consumption and exceptions to energy management and business processes DICE-FOPARA Matteo Cristani , Guido Governatori , Francesco Olivieri , Claudio Tomazzoli

	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	Causality, repairs and multi-agent systemsCREST at S6

16:00 45m Talk		Analysis, Repair and Causality for Timed Diagnostic Traces CREST Stefan Leue University of Konstanz File Attached
16:45 25m Research paper		Justification Based Reasoning in Dynamic Conflict Resolution [Werner Damm, Martin Franzle, Willem Hagemann, Paul Kroger, Astrid Rakow] CREST File Attached
17:10 25m Research paper		Towards A Logical Account of Epistemic Causality [Shakil M. Khan, Mikhail Soutchanski] CREST File Attached

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 Gina Belmonte , Vincenzo Ciancia , Diego Latella , Mieke Massink CNR-ISTI Pisa, Italy
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 Jérémy Dubut 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 Stefan Milius , Henning Urbat 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 Petar Vukmirović , Jasmin Blanchette Vrije Universiteit Amsterdam, Simon Cruanes , Stephan Schulz Link to publication

17:00 - 18:00	VitekMentoring Workshop at SUN II

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 Mahmoud Khaled TU Munich, Eric Kim , Murat Arcak , Majid Zamani
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 Olav Bunte , Jan Friso Groote , Jeroen J.A. Keiren , Maurice Laveaux , Thomas Neele , Erik P. de Vink , Wieger Wesselink , Anton Wijs Eindhoven University of Technology, Tim A.C. Willemse
19:08 3m Poster		Distributive Disjoint Polymorphism for Compositional Programming Posters Xuan Bi Standard Chartered Bank, Ningning Xie University of Toronto, 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 Karlheinz Friedberger , Marie-Christine Jakobs TU Darmstadt, Germany, Thomas Lemberger , Martin Spiessl , Philipp Wendler
19:22 3m Poster		DeepFault: Fault Localization for Deep Neural Networks Posters Hasan Ferit Eniser , Simos Gerasimou , Alper Sen
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 Aivo Toots , Reedik Tuuling , Maksym Yerokhin , Marlon Dumas , Luciano García-Bañuelos University of Tartu, Peeter Laud , Raimundas Matulevicius , Alisa Pankova , Martin Pettai , Pille Pullonen , Jake Tom
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 Pavel Andrianov , Pavel Andrianov , Pavel Andrianov
20:26 3m Poster		Constraint-based Monitoring of Hyperproperties Posters Bernd Finkbeiner , Christopher Hahn , Marvin Stenger , Leander Tentrup Saarland University

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	SemanticsFOSSACS at MOON Chair(s): C.-H. Luke Ong University of Oxford

10:30 30m Talk		Justness: A Completeness Criterion for Capturing Liveness Properties FOSSACS Rob van Glabbeek Link to publication
11:00 30m Talk		A Complete Normal-Form Bisimilarity for State FOSSACS Dariusz Biernacki University of Wrocław, Sergueï Lenglet University of Lorraine, France, Piotr Polesiuk University of Wrocław Link to publication
11:30 30m Talk		A Sound and Complete Logic for Algebraic Effects FOSSACS Cristina Matache , Sam Staton University of Oxford Link to publication
12:00 30m Talk		Strong Adequacy and Untyped Full-Abstraction for Probabilistic Coherence Spaces FOSSACS Thomas Leventis Università di Bologna, Michele Pagani University Paris Diderot Link to publication

10:30 - 12:30	SAT and SMT IITACAS at SUN I Chair(s): Armin Biere Johannes Kepler University Linz

10:30 30m Talk		Building Better Bit-Blasting for Floating-Point ProblemsBest paper nomination TACAS Martin Brain , Florian Schanda Zenuity, Youcheng Sun University of Oxford Link to publication
11:00 30m Talk		The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations TACAS Nils Becker , Peter Müller ETH Zurich, Alexander J. Summers ETH Zurich Link to publication
11:30 30m Talk		On the Empirical Time Complexity of Scale-Free 3-SAT at the Phase Transition TACAS Thomas Bläsius , Tobias Friedrich , Andrew Sutton Link to publication
12:00 30m Talk		Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework TACAS Ludovic Le Frioux , Souheib Baarir , Julien Sopena , Fabrice Kordon Sorbonne University — LIP6 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 University of Toronto, 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 Frédéric Gilbert 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	Resource LogicsFOSSACS at MOON Chair(s): Andrew M. Pitts University of Cambridge

14:00 30m Talk		A Dialectica-Like Interpretation of a Linear MSO on Infinite Words FOSSACS Colin Riba , Pierre Pradic Link to publication
14:30 30m Talk		Higher-order distributions for differential linear logic FOSSACS Marie Kerjean , Jean-Simon Lemay Link to publication
15:00 30m Talk		Causality in Linear Logic: Full Completeness and Injectivity (unit-free multiplicative-additive fragment) FOSSACS Simon Castellan Imperial College London, UK, Nobuko Yoshida Imperial College London Link to publication
15:30 30m Talk		Resource-Tracking Concurrent Games FOSSACS Aurore Alcolei , Pierre Clairambault CNRS & ENS Lyon, Olivier Laurent CNRS & ENS Lyon 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 Virgile Robles , Nikolai Kosmatov CEA List, Virgile Prevosto CEA Tech List, Pascale Le Gall 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	Demo ITACAS at 1st Floor Reception Area (Coffee)

16:30 90m Demonstration		Interactive session with tools and demos (I) TACAS

16:30 - 18:00	Model CheckingTACAS at SUN I Chair(s): Florian Zuleger Vienna University of Technology

16:30 30m Talk		VoxLogicA: a Spatial Model Checker for Declarative Image Analysis TACAS Gina Belmonte , Vincenzo Ciancia , Diego Latella , Mieke Massink CNR-ISTI Pisa, Italy Link to publication
17:00 30m Talk		On Reachability in Parameterized Phaser Programs TACAS Petru Eles , Zeinab Ganjei , Ludovic Henrio CNRS, Zebo Peng , Ahmed Rezine Link to publication
17:30 30m Talk		Abstract Dependency Graphs and Their Application to Model CheckingBest paper nomination TACAS Søren Enevoldsen , Kim Larsen Aalborg University, Jiri Srba 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	RepsMentoring Workshop at JUPITER

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	Model-driven Development and Model TransformationFASE at JUPITER Chair(s): Marielle Stoelinga University of Twente and Radboud University, Nijmegen

10:30 30m Talk		Pyro: Generating Domain-Specific Collaborative Online Modeling Environments FASE Philip Zweihoff , Stefan Naujokat , Bernhard Steffen Technical University Dortmund Link to publication
11:00 30m Talk		Efficient Model Synchronization by Automatically Constructed Repair ProcessesBest paper nomination FASE Lars Fritsche , Jens Kosiol , Andy Schürr TU Darmstadt, Gabriele Taentzer Universität Marburg Link to publication
11:30 30m Talk		Offline Delta-driven Model Transformation with Dependency Injection FASE Artur Boronat University of Leicester Link to publication
12:00 30m Talk		A Logic-Based Incremental Approach to Graph Repair FASE Sven Schneider , Leen Lambers , Fernando Orejas Universitat Politècnica de Catalunya, Spain Link to publication

10:30 - 12:30	Fixed-point LogicsFOSSACS at MOON Chair(s): Helmut Seidl Technische Universität München

10:30 30m Talk		Optimal Satisfiability Checking for Arithmetic mu-Calculi FOSSACS Daniel Hausmann , Lutz Schröder FAU Erlangen-Nürnberg, Lehrstuhl 8 Link to publication
11:00 30m Talk		Two-Way Parikh Automata with a Visibly Pushdown Stack FOSSACS Luc Dartois , Emmanuel Filiot , Jean-Marc Talbot Link to publication
11:30 30m Talk		Constructing Inductive-Inductive Types in Cubical Type Theory FOSSACS Jasper Hugunin Link to publication
12:00 30m Talk		Towards a Structural Proof Theory of Probabilistic mu–calculi FOSSACS Matteo Mio , Christophe Lucas Link to publication

10:30 - 12:30	Concurrent and Distributed SystemsTACAS at SUN I Chair(s): Marieke Huisman University of Twente

10:30 30m Talk		Multi-Core On-The-Fly Saturation TACAS Tom van Dijk University of Twente, Jeroen Meijer , Jaco van de Pol Aarhus University Link to publication
11:00 30m Talk		Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude TACAS Si Liu , Peter Ölveczky , Min Zhang East China Normal University, Qi Wang , José Meseguer Link to publication
11:30 30m Talk		The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and Usability TACAS Olav Bunte , Jan Friso Groote , Jeroen J.A. Keiren , Maurice Laveaux , Thomas Neele , Erik P. de Vink , Wieger Wesselink , Anton Wijs Eindhoven University of Technology, Tim A.C. Willemse Link to publication
12:00 30m Talk		Checking Deadlock-Freedom of Parametric Component-Based Systems TACAS Marius Bozga Verimag/CNRS, Radu Iosif VERIMAG, CNRS, Université Grenoble-Alpes, Joseph Sifakis Verimag/CNRS Link to publication

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	Demo IITACAS at 1st Floor Reception Area (Coffee)

13:00 60m Demonstration		Interactive session with tools and demos (II) TACAS

13:00 - 14:00	General AssemblySocial at SUN II

13:00 60m Meeting		ETAPS eV General Assembly Social

14:00 - 16:00	Software Verification IIFASE at JUPITER Chair(s): Heike Wehrheim Paderborn University

14:00 30m Talk		DeepFault: Fault Localization For Deep Neural Networks FASE Hasan Ferit Eniser , Simos Gerasimou , Alper Sen Link to publication
14:30 30m Talk		Variability Abstraction and Refinement for Game-based Lifted Model Checking of full CTL FASE Aleksandar S. Dimovski Mother Teresa University, Skopje, Axel Legay INRIA Rennes, Andrzej Wąsowski IT University of Copenhagen, Denmark Link to publication
15:00 30m Talk		Formal Verification of Safety & Security Related Timing Constraints for A Cooperative Automotive System FASE Huang Li , Eun-Young Kang University of Southern Denmark Link to publication
15:30 30m Talk		Checking Observational Purity Of Procedures FASE Himanshu Arora , Raghavan Komondoor Indian Institute of Science, Bangalore, G. Ramalingam Microsoft Research Link to publication

14:00 - 16:00	AutomataFOSSACS at MOON Chair(s): Thomas Colcombet IRIF, University Paris Diderot and CNRS, France

14:00 30m Talk		Identifiers in Registers – Describing Network Algorithms with Logic FOSSACS Benedikt Bollig CNRS, LSV, ENS Paris-Saclay, Patricia Bouyer LSV, CNRS & ENS Cachan, University Paris Saclay, Fabian Reiter Link to publication
14:30 30m Talk		Continuous Reachability for Unordered Data Petri Nets is in PTime FOSSACS Utkarsh Gupta , Preey Shah , S. Akshay , Piotr Hofman Link to publication
15:00 30m Talk		Languages ordered by the subword order FOSSACS Dietrich Kuske , Georg Zetzsche Max Planck Institute for Software Systems (MPI-SWS) Link to publication
15:30 30m Talk		Deciding Equivalence of Separated Non-Nested Attribute Systems in Polynomial Time FOSSACS Helmut Seidl Technische Universität München, Raphaela Palenta , Sebastian Maneth Link to publication

14:00 - 16:00	Hybrid and Stochastic SystemsTACAS at SUN I Chair(s): Kim Larsen Aalborg University

14:00 30m Talk		Tail Probabilities for Runtimes of Randomized Programs: Martingale Synthesis for Higher Moments TACAS Satoshi Kura , Natsuki Urabe , Ichiro Hasuo National Institute of Informatics Link to publication
14:30 30m Talk		Computing the Expected Execution Time of Probabilistic Workflow Nets TACAS Philipp J. Meyer , Javier Esparza , Philip Offtermatt Link to publication
15:00 30m Talk		Shepherding Hordes of Markov Chains TACAS Milan Ceska Brno University of Technology , Nils Jansen RWTH Aachen University, Sebastian Junges RWTH Aachen University, Germany, Joost-Pieter Katoen RWTH Aachen University Link to publication
15:30 30m Talk		Optimal Time-Bounded Reachability Analysis for Concurrent Systems TACAS Yuliya Butkova , Gereon Fox Link to publication

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 Rob van Glabbeek , Peter Höfner , Michael Markl Link to publication

16:30 - 18:00	Symbolic VerificationTACAS at SUN I Chair(s): Holger Hermanns Saarland University

16:30 30m Talk		iRank: a variable order metric for DEDS subject to linear invariants TACAS Elvio Gilberto Amparore , Gianfranco Ciardo , Susanna Donatelli , Andrew Miner Link to publication
17:00 30m Talk		Edge-Specified Reduction Binary Decision Diagrams TACAS Junaid Babar , Chuan Jiang , Gianfranco Ciardo , Andrew Miner Link to publication
17:30 30m Talk		Effective Entailment Checking for Separation Logic with Inductive Definitions TACAS Jens Katelaan , Christoph Matheja RWTH Aachen University, Florian Zuleger Vienna University of Technology Link to publication

17:00 - 18:00	WilhelmMentoring Workshop at JUPITER

17:00 60m Talk		Formal methods can be practical: Verifying time-critical systems Mentoring Workshop Reinhard Wilhelm Saarland University

19:30 - 23:00	BanquetSocial at Břevnovský klášter

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	Software Evolution & Requirements EngineeringFASE at JUPITER Chair(s): Gabriele Taentzer Universität Marburg

10:30 30m Talk		Structural and Nominal Cross-Language Clone Detection FASE Lawton Nichols , Mehmet Emre University of California, Santa Barbara, Ben Hardekopf UC Santa Barbara Link to publication
11:00 30m Talk		SL2SF: Refactoring Simulink to Stateflow FASE Stephen Wynn-Williams , Zinovy Diskin , Vera Pantelic , Mark Lawford McMaster, Gehan Selim , Curtis Milo Link to publication
11:30 30m Talk		Metric Temporal Graph Logic over Typed Attributed Graphs FASE Holger Giese Hasso Plattner Institute, University of Potsdam, Maria Maximova , Lucas Sakizloglou , Sven Schneider Link to publication
12:00 15m Talk		KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs FASE Qian Jiaqi , Min Zhang East China Normal University, Yi Wang Shenzhen University, Kazuhiro Ogata Link to publication
12:15 15m Talk		Business Process Privacy Analysis in PLEAK FASE Aivo Toots , Reedik Tuuling , Maksym Yerokhin , Marlon Dumas , Luciano García-Bañuelos University of Tartu, Peeter Laud , Raimundas Matulevicius , Alisa Pankova , Martin Pettai , Pille Pullonen , Jake Tom Link to publication

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	SynthesisTACAS at SUN I Chair(s): Roland Meyer Technical University of Braunschweig

10:30 30m Talk		Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware Approach TACAS Mahmoud Khaled TU Munich, Eric Kim , Murat Arcak , Majid Zamani Link to publication
11:00 30m Talk		StocHy: automated verification and synthesis of stochastic processes TACAS Nathalie Cauchi University of Oxford, Alessandro Abate University of Oxford Link to publication
11:30 30m Talk		Minimal-Time Synthesis for Parametric Timed Automata TACAS É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 Link to publication
12:00 30m Talk		Environmentally-friendly GR(1) Synthesis TACAS Rupak Majumdar MPI-SWS, Germany, Nir Piterman , Anne-Kathrin Schmuck 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 Nikita Chopra , R Rekha , Deepak D'Souza 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 Paul Dubrulle , Stéphane Louise , Christophe Gaston , Nikolai Kosmatov CEA List, Arnault Lapitre Link to publication

14:00 - 16:00	Privacy and ProtocolsPOST at MOON

14:00 30m Talk		*Wys: A DSL for Verified Secure Multi-party Computations** POST Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Michael Hicks University of Maryland, College Park Link to publication
14:30 30m Talk		Generalised Differential Privacy for Text Document Processing POST Natasha Fernandes , Mark Dras , Annabelle McIver Macquarie University Link to publication
15:00 30m Talk		Symbolic verification of distance bounding protocols POST Alexandre Debant , Stephanie Delaune Link to publication
15:30 30m Talk		On the formalisation of Σ-Protocols and Commitment Schemes POST David Butler , David Aspinall , Adria Gascon 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 Nikola Benes , Lubos Brim , Samuel Pastva , David Safranek Masaryk University 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

14:00 - 16:00	VerificationFOSSACS at SUN II Chair(s): Mikolaj Bojanczyk University of Warsaw

14:00 30m Talk		Tight Worst-Case Bounds for Polynomial Loop Programs FOSSACS Amir Ben-Amram , Geoff Hamilton Link to publication
14:30 30m Talk		Kleene algebra with hypotheses FOSSACS Amina Doumane , Denis Kuperberg , Damien Pous CNRS, Pierre Pradic Link to publication
15:00 30m Talk		The Impatient May Use Limited Optimism to Minimize Regret FOSSACS Michaël Cadilhac , Guillermo A. Perez University of Antwerp, Marie van den Bogaard Link to publication
15:30 30m Talk		Partial and Conditional Expectations in Markov Decision Processes with Integer Weights FOSSACS Jakob Piribauer , Christel Baier TU Dresden, Germany 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:30	Distributed SystemsPOST at MOON

16:30 30m Talk		Orchestrating Layered Attestations POST John D. Ramsdell , Paul D. Rowe , Perry Alexander , Sarah Helble , Peter Loscocco , J. Aaron Pendergrass , Adam Petz Link to publication
17:00 30m Talk		Verifying liquidity of Bitcoin contracts POST Massimo Bartoletti , Roberto Zunino Link to publication

16:30 - 18:00	Monitoring and Runtime VerificationTACAS at SUN I Chair(s): Ondřej Lengál Brno University of Technology

16:30 30m Talk		Specification and Efficient Monitoring Beyond STL TACAS Alexey Bakhirkin , Nicolas Basset Link to publication
17:00 30m Talk		VyPR2: A Framework for Runtime Verification of Python Web Services TACAS Joshua Dawes University of Manchester and CERN, Giles Reger University of Manchester, Giovanni Franzoni , Andreas Pfeiffer , Giacomo Govi Link to publication
17:30 30m Talk		Constraint-based Monitoring of Hyperproperties TACAS Christopher Hahn , Marvin Stenger , Leander Tentrup Saarland University 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

Get Calendar (iCal)

iCalendar subscription service for your personal schedule

You first need to have starred events () in order to use the iCalendar subscription service.

Currently Viewed Program

Downloads the currently viewed program (with filters applied) in iCal format

Session Calendar (ical)

session-calendar.ics

Detailed Event Calendar (ical)

event-calendar.ics

xMon 24 Nov 00:44

ETAPS 2019 Program

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

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

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

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

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

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

ETAPS 2019

Co-hosted Conferences

Workshops

ETAPS 2019 Program

Switch Program View

Program Display Configuration

Sat 6 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Sun 7 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Mon 8 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Tue 9 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Wed 10 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Thu 11 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Get Calendar (iCal)

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

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

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

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

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

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