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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30
09:00
60m
Talk
Invited talk by Margus Veanes
PERR
Margus VeanesMicrosoft Research
10:00
30m
Talk
Local Reasoning for Robust Observational Equivalence
PERR
Dan GhicaUniversity of Birmingham, Koko MuroyaRIMS, Kyoto University, JP & University of Birmingham, UK, Todd Waugh AmbridgeUniversity of Birmingham
09:00 - 10:30
IDICE-FOPARA at S11
Chair(s): Steffen JostLMU, 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 HedgesUniversity of Oxford
10:00
30m
Talk
Universal property of the monad for infinite trace strategies (work in progress)
GaLoP
Paul Blain LevyUniversity of Birmingham, Sergey GoncharovFAU Erlangen-Nürnberg, Lehrstuhl 8, Lutz SchöderFAU Erlangen-Nürnberg, Lehrstuhl 8
09:00 - 10:30
Mechanising Proofs for Behavioural Types and ProcessesBEHAPI at S4 (BEHAPI)
Chair(s): Antonio RavaraNOVA University of Lisbon and NOVA LINCS
09:00
30m
Talk
A Theory of Contexts for Higher-Order Encodings of Process Algebras
BEHAPI
Ivan ScagnettoUniversity of Udine
09:30
30m
Talk
Formalising session-typed languages without worries
BEHAPI
Wen KokkeUniversity of Edinburgh
10:00
30m
Talk
Adventures in Formalising the Meta-Theory of Session Types
BEHAPI
Francisco FerreiraImperial College London
09:00 - 10:30
CoCoTOOLympics at S5
09:00 - 10:30
Welcome & Keynote 1MeTRiD at S510
Chair(s): Simon BliudzeINRIA Lillle - Nord Europe, Panagiotis KatsarosITI-CERTH, Thessaloniki
09:15
15m
Day opening
Welcome
MeTRiD
Simon BliudzeINRIA Lillle - Nord Europe, Panagiotis KatsarosITI-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 MargariaUniversity of Limerick and Lero - The Irish Software Research Centre
09:00 - 10:30
09:00
30m
Talk
Welcome to InterAVT 2019
InterAVT
Stylianos BasagiannisUnited Technologies Research centre, Goetz BotterweckLero - The Irish Software Research Centre and University of Limerick, Anila MjedaLero - 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 FultonMIT-IBM Watson AI Lab
10:00
10m
Talk
Cross Programming Language Taint Analysis for the IoT Ecosystem
InterAVT
Pietro FerraraJuliaSoft SRL, Italy, Amit Kr MandalUniversità Ca' Foscari, Venezia, Italy, Agostino CortesiUniversità Ca' Foscari Venezia, Fausto SpotoU. Verona
10:10
10m
Talk
FVL: Formal Verification in the Loop to Enhance Verification of Safety-Critical Cyber-Physical Systems
InterAVT
Cinzia BernardeshiUniv. of Pisa, Andrea DomeniciUniversity of Pisa, Italy, Sergio SaponaraUniversity 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 CeskaBrno 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 KwiatkowskaUniversity of Oxford
10:10
10m
Short-paper
Poster flash: Comprehensive Modelling Platform
HSB
Matej TrojákMasaryk University, David SafranekMasaryk University, Jan ČervenýGlobal Change Research Institute CAS, Marek HavlíkMasaryk University, Lukrécia MertováMasaryk University, Matej HajnalMasaryk University, Jakub HrabecMasaryk University, Jakub ŠalagovičMasaryk University
10:20
10m
Short-paper
Poster flash: Formalizing metabolic-regulatory networks by hybrid automata
HSB
Lin LiuFreie Universität Berlin, Alexander BockmayrFreie 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-VeronaIMT Institute for Advanced Studies Lucca, Italy, Mirco TribastoneIMT Institute for Advanced Studies Lucca, Italy, Max TschaikowskiIMT Institute for Advanced Studies Lucca, Italy, Andrea VandinDTU, Denmark, Luca CardelliMicrosoft Research and University of Oxford
10:52
22m
Poster
Statistical abstraction for multi-scale spatio-temporal systems
Posters
Michalis MichaelidesUniversity of Edinburgh, Jane HillstonUniversity of Edinburgh, Guido SanguinettiUniversity of Edinburgh
11:14
22m
Poster
Towards Efficient Algorithms for Constraint Satisfaction Problems
Posters
Huu-Phuc VoUppsala University
11:36
22m
Poster
VIAP 1.1
Posters
11:58
22m
Poster
FreeST: context-free session types in a functional language
Posters
Bernardo AlmeidaUniversidade de Lisboa, Andreia MordidoLasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. VasconcelosUniversity of Lisbon, Portugal
12:20
22m
Poster
WAPS: Weighted and Projected Sampling
Posters
Rahul Gupta, Shubham Sharma, Subhajit RoyIIT Kanpur, India, Kuldeep S. MeelNational University of Singapore
12:42
22m
Poster
Semantic Fault Localization and Suspiciousness Ranking
Posters
Maria ChristakisMPI-SWS, Matthias HeizmannUniversity of Freiburg, Muhammad Numair MansurMax Planck Institute for Software Systems (MPI-SWS), Christian SchillingIST Austria, Valentin WüstholzConsenSys Diligence
13:04
22m
Poster
Ultimate Automizer
Posters
Matthias HeizmannUniversity of Freiburg, Yu-Fang ChenAcademia Sinica, Daniel DietschUniversity of Freiburg, Marius Greitschus, Jochen HoenickeUniversität Freiburg, Yong LiInstitute of Software, Chinese Academy of Sciences, Alexander NutzUniversity of Freiburg, Germany, Pavel Andrianov, Christian SchillingIST Austria, Tanja SchindlerUniversity of Freiburg, Andreas PodelskiUniversity 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 BloemenUniversity of Twente, Laure PetrucciUniversité Paris 13, Jaco van de PolAarhus University
14:32
22m
Poster
PeSCo: Predicting Sequential Combinations of Verifiers
Posters
Pavel Andrianov, Heike WehrheimPaderborn University
14:54
22m
Poster
CoVeriTest: Cooperative Verifier-Based Testing
Posters
Dirk BeyerLMU Munich, Marie-Christine JakobsTU Darmstadt, Germany
15:16
22m
Poster
JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)
Posters
Lucas CordeiroUniversity of Oxford, Daniel KroeningUniversity of Oxford, Peter SchrammelUniversity 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 RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.
11:00
30m
Talk
Data Representation Synthesis: Past, Present and Future
Mooly Fest
Alex AikenStanford University
11:30
30m
Talk
Mooly: Mensch, Marathon, Method, Magic
Mooly Fest
Thomas BallMicrosoft 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 JostLMU, 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 GallianiFree University of Bozen-Bolzano
11:30
30m
Talk
Logics for first-order definable team properties
GaLoP
Juha Kontinen, Fan YangUniversity of Helsinki
11:00 - 12:00
Mechanising Proofs of Behavioural Types for APIsBEHAPI at S4 (BEHAPI)
Chair(s): Luca PadovaniUniversity of Turin
11:00
20m
Talk
Proving properties about Linear Pi in Coq
BEHAPI
Antonio RavaraNOVA University of Lisbon and NOVA LINCS, Marco GiuntiNOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
11:20
20m
Talk
Binary Session Types in Coq
BEHAPI
Ornela DardhaUniversity of Glasgow
11:40
20m
Talk
Mechanise your proofs in Coq: From zero to cut-admissibility in less than three months.
BEHAPI
Marco CarboneIT 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 MargariaUniversity of Limerick and Lero - The Irish Software Research Centre
11:00
40m
Talk
Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries
MeTRiD
Nathalie BertrandINRIA Rennes, Igor KonnovInria Nancy, Marijana LazićTU Wien, Josef WidderTU Wien
11:40
40m
Talk
Revisiting the Glue of BIP
MeTRiD
Jacques CombazVerimag/CNRS
12:20
40m
Talk
Programming Dynamic Reconfigurable Systems with DR-BIP
MeTRiD
Rim El BallouliVerimag, Saddek BensalemVerimag, Marius BozgaVerimag/CNRS, Joseph SifakisVerimag/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 MjedaLero - The Irish Software Research Centre and University of Limerick, Goetz BotterweckLero - The Irish Software Research Centre and University of Limerick
11:20
10m
Talk
AskTheCode: Interactive Call Graph Exploration for Error Fixing and Prevention
InterAVT
11:30
30m
Talk
Lighting talks (non-authors)
InterAVT
11:00 - 12:30
ModellingHSB at S9
Chair(s): Tatjana PetrovUniversität Konstanz
11:00
30m
Talk
A Hybrid HMM Approach for the Dynamics of DNA Methylation
HSB
Charalampos KyriakopoulosSaarland University, Pascal GiehrSaarland University, Alexander LückSaarland University, Jörn WalterSaarland University, Verena WolfSaarland University
11:30
30m
Talk
Controlling noisy expression through auto regulation of burst frequency and protein stability
HSB
Pavol BokesComenius University, Abhyudai SinghUniversity of Delaware
12:00
30m
Talk
Using a hybrid approach to model central carbon metabolism across the cell cycle
HSB
Cecile MoulinLaboratoire de Recherche en Informatique, Université Paris-Saclay & UMR CNRS 8623, Laurent TournierMaIAGE, INRA, Université Paris-Saclay., Sabine PeresLaboratoire 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
IIIDICE-FOPARA at S11
Chair(s): Patrick BaillotCNRS & ENS Lyon
14:00
45m
Talk
Type-two Iteration with Bounded Query Revision
DICE-FOPARA
Bruce KapronUniversity of Victoria, Florian SteinbergINRIA Saclay
14:45
45m
Talk
Tiered complexity at higher order
DICE-FOPARA
Emmanuel Hainry, Bruce KapronUniversity of Victoria, Jean-Yves Marion LORIA, Romain PéchouxINRIA / 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 FijalkowCNRS, LaBRI, and Alan Turing Institute
14:30
30m
Talk
A Framework for Compositional Model Checking
GaLoP
Yu-Yang LinQueen Mary University of London, Nikos TzevelekosQueen Mary University of London
15:00
30m
Talk
Modalities as prices: a game model of intuitionistic linear logic with subexponentials
GaLoP
Timo LangVienna University of Technology, Chris FermüllerVienna University of Technology, Elaine PimentelFederal University of Rio Grande do Norte, Brazil, Carlos OlarteFederal University of Rio Grande do Norte, Brazil
13:30 - 15:30
Behavioural Types for API-based softwareBEHAPI at S4 (BEHAPI)
Chair(s): emilio tuostoUniversity of Leicester
13:30
30m
Talk
Mailbox Types for Unordered Interactions
BEHAPI
Ugo de'LiguoroUniversità di Torino, Luca PadovaniUniversity of Turin
14:00
30m
Talk
A Behavioural Type System for Mungo with Generics
BEHAPI
A: Hans HüttelDepartment of Computer Science, Aalborg University
14:30
30m
Talk
A Virtual-Machine Metaobject Protocol for Run-Time Software Adaptation
BEHAPI
Guido ChariCzech Technical University, Czechia
15:00
30m
Talk
Hardware Interactions as Behavioural Types.
BEHAPI
Francisco MartinsUniversity 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 ImmermanUniversity of Massachusetts, Amherst
14:30
30m
Talk
Concurrency Control Contract Composition
Mooly Fest
G. RamalingamMicrosoft Research
15:00
30m
Talk
Special Relations for Special Relationships
Mooly Fest
Nikolaj BjørnerMicrosoft Research
14:00 - 15:30
RERS 1TOOLympics at S5
14:00 - 15:30
Keynote 2MeTRiD at S510
Chair(s): Panagiotis KatsarosITI-CERTH, Thessaloniki
14:30
60m
Talk
Cyber-Physical Components as building blocks of more dependable industrial CPS
MeTRiD
Valeriy VyatkinAalto University, Finland and Luleå University of Technology, Sweden
14:00 - 15:30
Oded Maler memorial (1)HSB at S9
Chair(s): Nicola PaolettiRoyal Holloway, University of London, UK
14:00
60m
Talk
Oded Maler: An odyssey from Computer Science to Biological Sciences
HSB
Thao DangCNRS/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 UlbrichKarlsruhe Institute of Technology
16:30
30m
Talk
Proving Program Equivalence with Constrained Rewriting Induction and Ctrl
PERR
Carsten FuhsBirkbeck, University of London, Cynthia KopRadboud University Nijmegen, Naoki NishidaNagoya University
17:00
30m
Talk
Semantics-Based Proofs of Equivalence for Functions with Accumulators
PERR
Stefan CiobacaAlexandru Ioan Cuza University of Iasi, Dorel Lucanu, Sebastian Buruiana
16:00 - 18:00
BehAPI Business MeetingBEHAPI at S4 (BEHAPI)
Chair(s): Adrian FrancalanzaUniversity of Malta
16:00
60m
Talk
BehAPI Practices
BEHAPI
Caroline CaruanaUniversity of Malta
17:00
60m
Meeting
BehAPI Year 1 Review and Year 2 projections
BEHAPI
Adrian FrancalanzaUniversity of Malta
16:00 - 18:00
RERS 2TOOLympics at S5
16:00 - 18:00
Cyber-Physical Systems designMeTRiD at S510
Chair(s): Valeriy VyatkinAalto University, Finland and Luleå University of Technology, Sweden
16:00
40m
Talk
Localizing Faults in Simulink/Stateflow Models with STL
MeTRiD
Ezio BartocciTechnische Universität Wien, Thomas FerrèreIST Austria, Niveditha ManjunathAustrian Institute of Technology, Dejan NickovicAustrian Institute of Technology
16:40
40m
Talk
Model-based energy characterization of IoT system design aspects
MeTRiD
Alexios LekidisAristotle University of Thessaloniki
17:20
40m
Talk
Modeling and Simulation of Attacks on Cyber-physical Systems
MeTRiD
Cinzia BernardeshiUniv. 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 PaolettiRoyal Holloway, University of London, UK
16:00
60m
Talk
From Sensitive to Formal Barbaric Systems Biology
HSB
Alexandre DonzeUniversity of California, Berkeley
17:00
60m
Talk
Timed Patterns: from Definition to Matching and Monitoring, a survey in memoriam Oded Maler
HSB
Eugene AsarinIRIF, 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
Times are displayed in 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 PetrucciUniversité Paris 13, Jaco van de PolAarhus 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é MelliesCNRS and University Paris Diderot
10:00
30m
Talk
Simple game semantics and Day convolution
GaLoP
Clovis EberhartNational Institute of Informatics, Japan, Tom HirschowitzUniv. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry, Alexis LaouarUniv. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS
09:00 - 10:30
09:00 - 10:30
Session 1PLACES at S8
Chair(s): Francisco MartinsUniversity of Lisbon
09:00
60m
Talk
Keynote: Unstructured Parallelism Considered Harmful -- Using Structured Parallelism for Enhanced Software Verification
PLACES
Vivek SarkarRice University, USA
10:00
30m
Full-paper
A Message-Passing Interpretation of Adjoint Logic
PLACES
Klaas PruiksmaCarnegie Mellon University, Frank PfenningCarnegie Mellon University, USA
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. PerezUniversity of Antwerp, Leander TentrupSaarland University
09:00
60m
Tutorial
Reactive Synthesis Background and the Synthesis Competition
SYNT Camp
Guillermo A. PerezUniversity of Antwerp
10:00
30m
Tutorial
Hand-on Synthesis Experience with BoSy
SYNT Camp
Leander TentrupSaarland 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 BeyerLMU Munich, Marie-Christine JakobsTU Darmstadt, Germany
11:36
22m
Poster
FreeST: context-free session types in a functional language
Posters
Bernardo AlmeidaUniversidade de Lisboa, Andreia MordidoLasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. VasconcelosUniversity of Lisbon, Portugal
11:58
22m
Poster
JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)
Posters
Lucas CordeiroUniversity of Oxford, Daniel KroeningUniversity of Oxford, Peter SchrammelUniversity of Oxford, UK
12:20
22m
Poster
Markovian equivalences for biochemical reaction networks
Posters
Isabel Cristina Perez-VeronaIMT Institute for Advanced Studies Lucca, Italy, Mirco TribastoneIMT Institute for Advanced Studies Lucca, Italy, Max TschaikowskiIMT Institute for Advanced Studies Lucca, Italy, Andrea VandinDTU, Denmark, Luca CardelliMicrosoft 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 BloemenUniversity of Twente, Laure PetrucciUniversité Paris 13, Jaco van de PolAarhus University
13:04
22m
Poster
PeSCo: Predicting Sequential Combinations of Verifiers
Posters
Pavel Andrianov, Heike WehrheimPaderborn University
13:26
22m
Poster
Semantic Fault Localization and Suspiciousness Ranking
Posters
Maria ChristakisMPI-SWS, Matthias HeizmannUniversity of Freiburg, Muhammad Numair MansurMax Planck Institute for Software Systems (MPI-SWS), Christian SchillingIST Austria, Valentin WüstholzConsenSys Diligence
13:48
22m
Poster
Statistical abstraction for multi-scale spatio-temporal systems
Posters
Michalis MichaelidesUniversity of Edinburgh, Jane HillstonUniversity of Edinburgh, Guido SanguinettiUniversity 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 VoUppsala University
14:54
22m
Poster
Ultimate Automizer
Posters
Matthias HeizmannUniversity of Freiburg, Yu-Fang ChenAcademia Sinica, Daniel DietschUniversity of Freiburg, Marius Greitschus, Jochen HoenickeUniversität Freiburg, Yong LiInstitute of Software, Chinese Academy of Sciences, Alexander NutzUniversity of Freiburg, Germany, Pavel Andrianov, Christian SchillingIST Austria, Tanja SchindlerUniversity of Freiburg, Andreas PodelskiUniversity 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 RoyIIT Kanpur, India, Kuldeep S. MeelNational 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 RajanUniversity of Edinburgh
11:00
30m
Talk
Navigating through the academic jungle: tips, tricks & traps
Mentoring Workshop
Marielle StoelingaUniversity of Twente and Radboud University, Nijmegen
11:30
30m
Talk
Push, Pull, Partner - A Few Models for Industrial Research
Mentoring Workshop
Thomas BallMicrosoft Research
11:00 - 12:00
11:00
60m
Talk
(Invited Talk) Cons-free Rewriting
DICE-FOPARA
Cynthia KopRadboud 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 ScalasAston University, Nobuko YoshidaImperial College London
11:30
30m
Talk
Probabilistic Programming Inference via Intensional Semantics
GaLoP
Simon CastellanImperial College London, UK, Hugo PaquetUniversity of Cambridge
11:00 - 12:00
IIHCVS at S4 (HCVS)
Chair(s): Mattias UlbrichKarlsruhe Institute of Technology
11:00
30m
Talk
Challenges in the specialisation of smart Horn clause interpreters
HCVS
John P. GallagherRoskilde University
File Attached
11:30
30m
Full-paper
Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification
HCVS
Emanuele De AngelisUniversity of Chieti-Pescara, Fabio FioravantiUniversity of Chieti-Pescara, Alberto PettorossiUniversity of Rome Tor Vergata, Italy, Maurizio ProiettiCNR-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 KretinskyTechnical University of Munich
11:30
30m
Talk
Static Analysis for the OWASP IoT Top 10 2018.
SPIoT
Pietro FerraraJuliaSoft SRL, Italy, Amit Kr MandalUniversità Ca' Foscari, Venezia, Italy, Agostino CortesiUniversità Ca' Foscari Venezia, Fausto SpotoU. Verona
12:00
30m
Talk
The Refinement-Risk Loop - A Process for Security Engineering in Isabelle
SPIoT
Florian KammüllerMiddlesex University, UK
11:00 - 12:00
IIPLACES at S8
Chair(s): Ornela DardhaUniversity of Glasgow
11:00
30m
Full-paper
FreeST: context-free session types in a functional language
PLACES
Bernardo AlmeidaUniversidade de Lisboa, Andreia MordidoLasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. VasconcelosUniversity of Lisbon, Portugal
11:30
30m
Full-paper
Concurrent Typestate-Oriented Programming in Java
PLACES
Rosita GerboUniversità di Torino, Luca PadovaniUniversity of Turin
11:00 - 12:30
AnalysisHSB at S9
Chair(s): Jerome FeretINRIA Paris
11:00
30m
Talk
Fixed-point Computation of Equilibria in Biochemical Regulatory Networks
HSB
Isabel Cristina Perez-VeronaIMT Institute for Advanced Studies Lucca, Italy, Mirco TribastoneIMT Institute for Advanced Studies Lucca, Italy, Max TschaikowskiIMT Institute for Advanced Studies Lucca, Italy
11:30
30m
Talk
Rejection-Based Simulation of Stochastic Spreading Processes on Complex Networks
HSB
Gerrit GroßmannSaarland University, Verena WolfSaarland University
12:00
30m
Talk
rPrism -- A software for reactive weighted state transition models
HSB
Daniel FigueiredoUniversity of Aveiro, Eugénio A. M. RochaUniversity of Aveiro, Madalena ChavesINRIA, Manuel A. MartinsUniversity 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. PerezUniversity of Antwerp, Leander TentrupSaarland University
11:00
60m
Tutorial
Hand-on Synthesis Experience with BoSy (part 2)
SYNT Camp
Leander TentrupSaarland University
13:30 - 15:30
VIIDICE-FOPARA at S11
Chair(s): Marko van EekelenOpen University of the Netherlands
14:00
45m
Talk
Modular Runtime Complexity Analysis of Probabilistic While Programs
DICE-FOPARA
Martin AvanziniINRIA Sophia Antipolis, France, Michael SchaperUniversity of Innsbruck, Georg MoserUniversity 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. GallagherRoskilde 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 BasoldCNRS & ENS Lyon, Ekaterina KomendantskayaHeriot-Watt University, UK
Link to publication
15:00
30m
Full-paper
Ultimate TreeAutomizer
HCVS
Daniel DietschUniversity of Freiburg, Matthias HeizmannUniversity of Freiburg, Jochen HoenickeUniversität Freiburg, Alexander NutzUniversity of Freiburg, Germany, Andreas PodelskiUniversity of Freiburg, Germany
13:30 - 15:30
IIIPLACES at S8
Chair(s): Vasco VasconcelosLASIGE, Faculty of Sciences, University of Lisbon
13:30
60m
Talk
Keynote: Shared Session Types for Safe, Practical Concurrency
PLACES
Stephanie BalzerCarnegie Mellon University
14:30
30m
Full-paper
Multiparty session type-safe web development with static linearity
PLACES
Jonathan KingHabito and Imperial College London, Nicholas NgImperial College London, Nobuko YoshidaImperial College London
15:00
30m
Full-paper
Service Equivalence via Multiparty Session Type Isomorphisms
PLACES
Assel AltayevaImperial College London, Nobuko YoshidaImperial 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 HuismanUniversity of Twente
14:30
30m
Talk
Advice on your adviser
Mentoring Workshop
Marsha ChechikUniversity of Toronto
File Attached
15:00
30m
Talk
A few lessons from the PhD I just finished
Mentoring Workshop
Juliana FrancoMicrosoft 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 HansenAalborg University, Denmark, Peter Gjøl JensenAalborg University, Denmark, Kim LarsenAalborg University, Axel LegayINRIA Rennes, Danny Bøgsted PoulsenUniversity of Kiel, Germany
14:30
30m
Talk
Learning from attacks and failures: generating reliability models from data
SPIoT
Marielle StoelingaUniversity of Twente and Radboud University, Nijmegen
15:00
30m
Talk
Graph-based Technique for Survivability Estimation and Optimization of IoT Applications
SPIoT
Vladimir ShakhovUniversity of Ulsan, South Korea, Insoo KooUniversity of Ulsan, South Korea
14:00 - 15:30
Algebraic approaches to causalityCREST at S6
14:00
45m
Talk
Coalgebras for causality
CREST
Matteo SammartinoUniversity College London
File Attached
14:45
45m
Talk
Causality and diagrammatic reasoning
CREST
16:00 - 18:00
VIIIGaLoP at S3
16:00 - 18:00
IVHCVS at S4 (HCVS)
Chair(s): Nikolaj BjørnerMicrosoft Research
16:00
30m
Talk
Decomposing Farkas Interpolants
HCVS
Martin BlichaUSI Lugano, Switzerland, Antti Hyvärinen, Jan KofroňCharles University, Natasha SharyginaUSI Lugano, Switzerland
File Attached
16:30
30m
Experience report
Report on the CHC competition
HCVS
Grigory FedyukovichPrinceton 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 HuismanUniversity of Twente, P: Rance CleavelandUniversity of Maryland, P: Holger HermannsSaarland University, P: Kim LarsenAalborg University, M: Bernhard SteffenTechnical 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 BatzRWTH Aachen University, Benjamin Lucien KaminskiRWTH Aachen University; University College London, Joost-Pieter KatoenRWTH Aachen University, Christoph MathejaRWTH Aachen University, Thomas NollRWTH Aachen University
DOI
16:30
30m
Talk
An Adequate Semantics for Hybrid While
QAPL
Sergey GoncharovFAU Erlangen-Nürnberg, Lehrstuhl 8, Renato NevesUniversity 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 BernardoUniversity of Urbino
16:00 - 18:00
IVPLACES at S8
Chair(s): Francisco MartinsUniversity of Lisbon
16:00
30m
Full-paper
Value-Dependent Session Design in a Dependently Typed Language
PLACES
Jan de Muijnck-HughesUniversity of Glasgow, Edwin BradyUniversity of St. Andrews, UK, Wim VanderbauwhedeUniversity of Glasgow
16:30
30m
Talk
Fluid Types: Statically Verified Distributed Protocols with Refinements
PLACES
Fangyi ZhouImperial College London, Francisco FerreiraImperial College London, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial 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 ChiappaloneItalian Institute of Technology
16:00
30m
Talk
Extracting landscape features from single particle trajectories
HSB
Ádám HalászWest Virginia University, Ouri MalerWest Virginia University, Jeremy S EdwardsUniversity of New Mexico
16:30
30m
Talk
Fuzzy Matching in Symbolic Systems Biology
HSB
Adrian RiescoUniversidad Complutense de Madrid, Beatriz Santos-BuitragoSeoul National University, Merrill KnappSRI International, Gustavo Santos-GarciaUniversidad de Salamanca, Carolyn TalcottSRI International
17:00
30m
Talk
Data-informed parameter synthesis for population Markov chains
HSB
Matej HajnalMasaryk University, Tatjana PetrovUniversität Konstanz, David SafranekMasaryk University, Morgane NouvianUniversity 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 BalzerCarnegie Mellon University, Barbora BuhnovaMasaryk University, Juliana FrancoMicrosoft Research, Cambridge

Mon 8 Apr
Times are displayed in 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 KatoenRWTH Aachen University, Jan VitekNortheastern University and Czech Technical University, Jan KofroňCharles University
09:00 - 10:00
ChechikKeynotes at SUN I
Chair(s): Joost-Pieter KatoenRWTH Aachen University
09:00
60m
Talk
Software Assurance in an Uncertain World
Keynotes
Marsha ChechikUniversity of Toronto
Link to publication File Attached
10:30 - 12:30
Applied CategoriesFOSSACS at MOON
Chair(s): Alex SimpsonUniversity 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önigUniversity of Duisburg-Essen, Dennis NolteUniversity of Duisburg-Essen, Arend RensinkUniversity of Twente, The Netherlands
Link to publication
11:30
30m
Talk
Change Actions: Models of Generalised Differentiation
FOSSACS
Mario Alvarez-PicalloUniversity of Oxford, C.-H. Luke OngUniversity of Oxford
Link to publication
12:00
30m
Talk
Causal Inference by String Diagram Surgery
FOSSACS
Aleks KissingerRadboud University, Bart JacobsRadboud University Nijmegen, Fabio ZanasiUniversity College London
Link to publication
10:30 - 12:30
SAT and SMT ITACAS at SUN I
Chair(s): Lijun ZhangChinese Academy of Sciences
10:30
30m
Talk
Decomposing Farkas Interpolants
TACAS
Martin BlichaUSI Lugano, Switzerland, Antti Hyvärinen, Jan KofroňCharles University, Natasha SharyginaUSI Lugano, Switzerland
Link to publication
11:00
30m
Talk
Parallel SAT Simplification on GPU Architectures
TACAS
Muhammad OsamaEindhoven University of Technology, Anton WijsEindhoven University of Technology
Link to publication
11:30
30m
Talk
Encoding Redundancy for Satisfaction-Driven Clause LearningBest paper nomination
TACAS
Marijn HeuleThe University of Texas at Austin, Benjamin KieslCISPA Helmholtz Center for Information Security, Armin BiereJohannes Kepler University Linz
Link to publication
12:00
30m
Talk
WAPS: Weighted and Projected Sampling
TACAS
Rahul Gupta, Shubham Sharma, Subhajit RoyIIT Kanpur, India, Kuldeep S. MeelNational University of Singapore
Link to publication
10:30 - 12:30
Program VerificationESOP at SUN II
Chair(s): Luís CairesNOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
10:30
30m
Talk
Time Credits and Time Receipts in Iris
ESOP
Glen Mével, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, François PottierInria, France
Link to publication
11:00
30m
Talk
Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms
ESOP
Guido MartínezCIFASIS-CONICET, Argentina, Danel AhmanUniversity of Ljubljana, Victor DumitrescuNomadic Labs Paris, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Cătălin HriţcuInria Paris, Monal NarasimhamurthyUniversity of Colorado, Boulder, Zoe ParaskevopoulouPrinceton University, Clément Pit-ClaudelMIT CSAIL, Jonathan ProtzenkoMicrosoft Research, Redmond, Tahina RamananandroMicrosoft Research, n.n., Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research
Link to publication
11:30
30m
Talk
Semi-Automated Reasoning About Non-Determinism in C Expressions
ESOP
Dan FruminRadboud University, Léon GondelmanLRI, Université Paris-Sud, Robbert KrebbersDelft 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 JonesIOHK, Mario Alvarez-PicalloUniversity of Oxford, Alexander Eyers-TaylorSemmle, C.-H. Luke OngUniversity of Oxford
Link to publication
14:00 - 16:00
Categories and (Co)algebraFOSSACS at MOON
Chair(s): Sergey GoncharovFAU 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ógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity 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, Jérémy Dubut, Shin-ya KatsumataNational Institute of Informatics, Ichiro HasuoNational Institute of Informatics
Link to publication
15:30
30m
Talk
Coalgebra Learning via Duality
FOSSACS
Simone Barlocco, Clemens KupkeUniversity of Strathclyde, Jurriaan RotRadboud University Nijmegen
Link to publication
14:00 - 16:00
Verification and AnalysisTACAS at SUN I
Chair(s): Dirk BeyerLMU Munich
14:00
30m
Talk
LCV: A Verification Tool for Linear Controller Software
TACAS
Junkil ParkUniversity of Pennsylvania, Miroslav PajicDuke University, Oleg SokolskyUniversity of Pennsylvania, USA, Insup Lee
Link to publication
14:30
30m
Talk
Semantic Fault Localization and Suspiciousness Ranking
TACAS
Maria ChristakisMPI-SWS, Matthias HeizmannUniversity of Freiburg, Muhammad Numair MansurMax Planck Institute for Software Systems (MPI-SWS), Christian SchillingIST Austria, Valentin WüstholzConsenSys Diligence
Link to publication
15:00
30m
Talk
Computing Coupled Similarity
TACAS
Benjamin BispingTechnische Universität Berlin, Uwe Nestmann
Link to publication
15:30
30m
Talk
Reachability Analysis for Termination and Confluence of Rewriting
TACAS
Christian SternagelUniversity of Innsbruck, Austria, Akihisa Yamada
Link to publication
14:00 - 16:00
Language DesignESOP at SUN II
Chair(s): Atsushi IgarashiKyoto University, Japan
14:00
30m
Talk
Codata in Action
ESOP
Paul DownenUniversity of Oregon, USA, Zachary Sullivan, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft, UK
Link to publication
14:30
30m
Talk
Composing bidirectional programs monadically
ESOP
Li-yao XiaUniversity of Pennsylvania, Dominic OrchardUniversity of Kent, UK, Meng WangUniversity of Bristol, UK
Link to publication
15:00
30m
Talk
Counters in Kappa: Semantics, Simulation, and Static Analysis
ESOP
Link to publication
15:30
30m
Talk
One Step at a Time
ESOP
Kathleen FisherTufts University, Ferdinand VeselySwansea University
Link to publication
16:30 - 18:00
TinelliTutorials at MOON
Chair(s): Fabrice KordonSorbonne University — LIP6
16:30
90m
Talk
An overview of Satisfiability Modulo Theories and its applications
Tutorials
Cesare TinelliUniversity of Iowa
Link to publication
16:30 - 18:00
SAT Solving and Theorem ProvingTACAS at SUN I
Chair(s): Armin BiereJohannes 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 ChenBirkbeck, University of London
Link to publication
17:00
30m
Talk
Incremental Analysis of Evolving Alloy Models
TACAS
Wenxi WangThe University of Texas at Austin, Texas, USA, Kaiyuan WangGoogle, Inc., Milos GligoricUniversity of Texas at Austin, Sarfraz KhurshidUniversity 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 VitekNortheastern 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 SiekCzech Technical University in Prague
18:30
3m
Poster
Partial and Conditional Expectations in Markov Decision Processes with Integer Weights
Posters
Jakob Piribauer, Christel BaierTU Dresden, Germany
18:33
3m
Poster
Information Flow Control Parallel Runtime Systems Foundations
Posters
Marco VassenaChalmers University of Technology, Deian StefanUniversity of California San Diego
18:37
3m
Poster
VyPR2: A Framework for Runtime Verification of Python Web Services
Posters
Joshua DawesUniversity of Manchester and CERN, Giles RegerUniversity 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 AltayevaImperial College London, Nobuko YoshidaImperial College London
18:44
3m
Poster
Tool Support for Correctness-by-Construction
Posters
Tobias RungeTU Braunschweig, Thomas ThümUniversity of Ulm, Loek CleophasEindhoven University of Technology (TU/e) and Stellenbosch University (SU), Ina SchaeferTechnische Universität Braunschweig, Bruce W Watson, Derrick KourieStellenbosch University
18:47
3m
Poster
Verifiably Safe Off-Model Reinforcement Learning
Posters
Nathan FultonMIT-IBM Watson AI Lab, André PlatzerCarnegie 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 AlmeidaUniversidade de Lisboa, Andreia MordidoLasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. VasconcelosUniversity of Lisbon, Portugal
18:58
3m
Poster
WAPS: Weighted and Projected Sampling
Posters
Rahul Gupta, Shubham Sharma, Subhajit RoyIIT Kanpur, India, Kuldeep S. MeelNational University of Singapore
19:01
3m
Poster
Semantic Fault Localization and Suspiciousness Ranking
Posters
Maria ChristakisMPI-SWS, Matthias HeizmannUniversity of Freiburg, Muhammad Numair MansurMax Planck Institute for Software Systems (MPI-SWS), Christian SchillingIST Austria, Valentin WüstholzConsenSys 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 BiStandard Chartered Bank, Ningning XieThe University of Hong Kong, Bruno C. d. S. OliveiraThe University of Hong Kong, Hong Kong, Tom SchrijversKU Leuven
19:12
3m
Poster
Ultimate Automizer
Posters
Matthias HeizmannUniversity of Freiburg, Yu-Fang ChenAcademia Sinica, Daniel DietschUniversity of Freiburg, Marius Greitschus, Jochen HoenickeUniversität Freiburg, Yong LiInstitute of Software, Chinese Academy of Sciences, Alexander NutzUniversity of Freiburg, Germany, Pavel Andrianov, Christian SchillingIST Austria, Tanja SchindlerUniversity of Freiburg, Andreas PodelskiUniversity of Freiburg, Germany
19:15
3m
Poster
Automatically Identifying Sufficient Object Builders from Module APIs
Posters
Pablo PonzioDept. of Computer Science FCEFQyN, University of Rio Cuarto, Valeria BengoleaDept. of Computer Science FCEFQyN, University of Rio Cuarto, Mariano Politano, Nazareno AguirreDept. of Computer Science FCEFQyN, University of Rio Cuarto, Marcelo F. FriasDept. 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 SchubertHeinz Nixdorf Institut, Paderborn University, Ben HermannUniversity of Paderborn, Eric BoddenHeinz Nixdorf Institut, Paderborn University and Fraunhofer IEM
19:30
3m
Poster
Credential Scanning powered by Symbolic Regex Matching
Posters
Margus VeanesMicrosoft Research, Olli Saarikivi, Eric XuMicrosoft, USA, Tiki Wan, Arvind RaviMicrosoft Azure
19:33
3m
Poster
ROLL 1.0: $\omega$-Regular Language Learning Library
Posters
Yong LiInstitute of Software, Chinese Academy of Sciences, Xuechao Sun, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Yu-Fang ChenAcademia Sinica, Junnan Xu
19:37
3m
Poster
Parallel SAT Simplification on GPU Architectures
Posters
Muhammad OsamaEindhoven University of Technology, Anton WijsEindhoven University of Technology
19:40
3m
Poster
Computing Coupled Similarity
Posters
Benjamin BispingTechnische 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 BoerCentrum Wiskunde & Informatica, Leiden University, Einar Broch JohnsenUniversity of Oslo, Violet Ka I Pun, Silvia Lizeth Tapia TarifaUniversity of Oslo
19:47
3m
Poster
Minimal-Time Synthesis for Parametric Timed Automata
Posters
Étienne AndréLIPN, CNRS UMR 7030, Université Paris 13, Vincent BloemenUniversity of Twente, Laure PetrucciUniversité Paris 13, Jaco van de PolAarhus University
19:51
3m
Poster
PeSCo: Predicting Sequential Combinations of Verifiers
Posters
Pavel Andrianov, Heike WehrheimPaderborn University
19:54
3m
Poster
The COMPASS 3.0 Toolset
Posters
Marco Bozzano, Harold Bruintjes, Alessandro CimattiFondazione Bruno Kessler, Joost-Pieter KatoenRWTH Aachen University, Thomas NollRWTH Aachen University, Stefano TonettaFondazione Bruno Kessler, Italy
19:58
3m
Poster
CoVeriTest: Cooperative Verifier-Based Testing
Posters
Dirk BeyerLMU Munich, Marie-Christine JakobsTU Darmstadt, Germany
20:01
3m
Poster
Decomposing Farkas Interpolants
Posters
Martin BlichaUSI Lugano, Switzerland, Antti Hyvärinen, Jan KofroňCharles University, Natasha SharyginaUSI Lugano, Switzerland
20:05
3m
Poster
ILAng: A Modeling and Verification Platform for SoCs using Instruction-Level Abstractions
Posters
Bo-Yuan HuangPrinceton University, USA, Hongce Zhang, Aarti GuptaPrinceton University, Sharad MalikPrinceton University
20:08
3m
Poster
JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)
Posters
Lucas CordeiroUniversity of Oxford, Daniel KroeningUniversity of Oxford, Peter SchrammelUniversity of Oxford, UK
20:12
3m
Poster
CLTestCheck: Measuring Test Effectiveness for GPU Kernels
Posters
Chao PengUniversity of Edinburgh, UK, Ajitha RajanUniversity 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 StoilkovskaVienna University of Technology , Igor KonnovInria Nancy, Josef WidderTU Wien, Florian ZulegerVienna 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
Times are displayed in 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 BojanczykUniversity of Warsaw
09:00
60m
Talk
On infinite duration games
Keynotes
Thomas ColcombetIRIF, 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 AalstRWTH Aachen
10:30
30m
Talk
Tool Support for Correctness-by-Construction
FASE
Tobias RungeTU Braunschweig, Ina SchaeferTechnische Universität Braunschweig, Loek CleophasEindhoven University of Technology (TU/e) and Stellenbosch University (SU), Thomas ThümUniversity of Ulm, Derrick KourieStellenbosch University, Bruce W Watson
Link to publication
11:00
30m
Talk
Automatic Modeling for Opaque Code in JavaScript Static Analysis
FASE
Joonyoung Park, Alexander JordanOracle Labs, Australia, Sukyoung RyuKAIST, South Korea
Link to publication
11:30
30m
Talk
SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language
FASE
Min ZhangEast China Normal University, Fu Song, Frederic MalletUniversité 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 HennickerLudwig Maximilians University Munich, Germany, Alexandre Madeira, Alexander Knapp
Link to publication
10:30 - 12:30
TypesESOP at SUN II
Chair(s): Vasco VasconcelosLASIGE, Faculty of Sciences, University of Lisbon
10:30
30m
Talk
Handling polymorphic algebraic effects
ESOP
Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan
Link to publication
11:00
30m
Talk
Distributive Disjoint Polymorphism for Compositional Programming
ESOP
Xuan BiStandard Chartered Bank, Ningning XieThe University of Hong Kong, Bruno C. d. S. OliveiraThe University of Hong Kong, Hong Kong, Tom SchrijversKU Leuven
Link to publication
11:30
30m
Talk
Types by Need
ESOP
Beniamino AccattoliInria & Ecole Polytechnique, Giulio GuerrieriUniversity 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 SteffenTechnical University Dortmund
14:00
30m
Talk
Omega-Regular Objectives in Model-Free Reinforcement Learning
TACAS
Ernst Moritz HahnQueen's University Belfast, Mateo Perez, Sven ScheweUniversity of Liverpool, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak
Link to publication
14:30
30m
Talk
Verifiably Safe Off-Model Reinforcement Learning
TACAS
Nathan FultonMIT-IBM Watson AI Lab, André PlatzerCarnegie Mellon University
Link to publication
14:00 - 16:00
Tool DemosTACAS at SUN I
Chair(s): Marius MikucionisAalborg University
14:00
15m
Talk
nonreach – A Tool for Nonreachability Analysis
TACAS
Florian Messner, Christian SternagelUniversity of Innsbruck, Austria
Link to publication
14:15
15m
Talk
The Quantitative Verification Benchmark Set
TACAS
Arnd HartmannsUniversity of Twente, Michaela KlauckSaarland Informatics Campus, Saarland University, David ParkerUniversity of Birmingham, Tim QuatmannRWTH 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 HuangPrinceton University, USA, Hongce Zhang, Aarti GuptaPrinceton University, Sharad MalikPrinceton 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 ChenAcademia Sinica, Yong LiInstitute of Software, Chinese Academy of Sciences, Xuechao Sun, Andrea TurriniState 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 VeanesMicrosoft Research, Olli Saarikivi, Eric XuMicrosoft, USA, Tiki Wan
Link to publication
15:30
15m
Talk
COMPASS 3.0
TACAS
Marco Bozzano, Harold Bruintjes, Alessandro CimattiFondazione Bruno Kessler, Joost-Pieter KatoenRWTH Aachen University, Thomas NollRWTH Aachen University, Stefano TonettaFondazione Bruno Kessler, Italy
Link to publication
15:45
15m
Talk
Debugging of Behavioural Models with CLEAR
TACAS
Gianluca BarbonUniversit� Grenoble Alpes, Inria, LIG, Vincent LeroyUniversity of Grenoble - CNRS, Gwen SalaünUniversity of Grenoble Alpes
Link to publication
14:00 - 16:00
Program SemanticsESOP at SUN II
Chair(s): Andrzej MurawskiUniversity of Oxford
14:00
30m
Talk
Extended call-by-push-value: reasoning about effectful programs and evaluation orderBest paper nomination
ESOP
Dylan McDermottUniversity of Cambridge, Alan MycroftUniversity of Cambridge
Link to publication
14:30
30m
Talk
Effectful Normal-Form Bisimulation
ESOP
Ugo Dal LagoUniversity of Bologna / Inria, Francesco Gavazzo
Link to publication
15:00
30m
Talk
On the Multi-Language Construction
ESOP
Samuele BuroUniversità degli Studi di Verona, Isabella MastroeniUniversity of Verona, Italy
Link to publication
15:30
30m
Talk
Probabilistic Programming Inference via Intensional Semantics
ESOP
Simon CastellanImperial College London, UK, Hugo PaquetUniversity of Cambridge
Link to publication
16:30 - 18:00
BeyerTutorials at SUN II
Chair(s): Joost-Pieter KatoenRWTH Aachen University
16:30
90m
Talk
Software Verification — An Overview of the State of the Art
Tutorials
Dirk BeyerLMU Munich
File Attached
17:00 - 18:00
17:00
60m
Talk
A tale of two MURIs: Authorization Meets Model Checking
Mentoring Workshop
Thomas RepsUniversity 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 KatoenRWTH Aachen University, Holger HermannsSaarland University, Gilles BartheIMDEA Software Institute, Gerald LüttgenUniversity of Bamberg, Tarmo UustaluReykjavik University, Vladimiro SassoneUniversity of Southampton, Lenore ZuckUniversity of Illinois at Chicago, Luís CairesNOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa, Peter MüllerETH Zurich, Peter ThiemannUniversity of Freiburg, Germany, Reiner HähnleTechnical University of Darmstadt, Wil van der AalstRWTH Aachen, Heike WehrheimPaderborn University, Jordi CabotICREA - UOC, Gabriele TaentzerUniversität Marburg, Mikolaj BojanczykUniversity of Warsaw, Alex SimpsonUniversity of Ljubljana, Barbara KönigUniversity of Duisburg-Essen, Andrew PittsUniversity of Cambridge, Flemming NielsonTechnical University of Denmark, Dave SandsChalmers, Matteo MaffeiTU Wien, Tomáš VojnarBrno University of Technology, Lijun ZhangChinese Academy of Sciences, Armin BiereJohannes Kepler University Linz, David ParkerUniversity of Birmingham, Kim LarsenAalborg University, Panagiotis KatsarosITI-CERTH, Thessaloniki, Jan VitekNortheastern University and Czech Technical University, Jan KofroňCharles University, Tiziana MargariaUniversity of Limerick and Lero - The Irish Software Research Centre , Anton WijsEindhoven University of Technology, Jurriaan HageUtrecht University, Reiko HeckelUniversity of Leicester, Catuscia PalamidessiINRIA and LIX, Don SannellaUniversity of Edinburgh

Wed 10 Apr
Times are displayed in 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 CairesNOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
09:00
60m
Talk
From quadcopters to helicopters: Formal verification to eliminate exploitable bugs
Keynotes
Kathleen FisherTufts University
File Attached
10:30 - 12:30
Security and Incremental ComputationESOP at SUN II
Chair(s): Zhong ShaoYale University
10:30
30m
Talk
Robustly Safe Compilation
ESOP
Marco PatrignaniStanford University & CISPA Helmholtz Center for Information Security, Deepak GargMax 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 BlazyUniv Rennes- IRISA, Alexandre Dang, Thomas P. JensenINRIA Rennes, Pierre WilkeYale University
Link to publication
11:30
30m
Talk
Safe Deferred Memory Reclamation with Types
ESOP
Ismail KuruDrexel University, Colin GordonDrexel University
Link to publication
12:00
30m
Talk
Incremental λ-Calculus in Cache-Transfer Style, Static Memoization by Program Transformation
ESOP
Paolo G. GiarrussoTU Delft, The Netherlands, Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Philipp SchusterUniversity 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
17:00 - 18:00
17:00
60m
Talk
Formal methods can be practical: Verifying time-critical systems
Mentoring Workshop
Reinhard WilhelmSaarland University
19:30 - 23:00
19:30
3h30m
Social Event
Banquet
Social
Jan KofroňCharles University

Thu 11 Apr
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
FlanaganKeynotes at SUN I
Chair(s): Tomáš VojnarBrno University of Technology
09:00
60m
Talk
Towards Efficient and Precise Concurrent Software Analysis
Keynotes
Cormac FlanaganUniversity 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 VassenaChalmers University of Technology, Gary Soeller, Peter Amidon, Matthew Chan, John RennerUniversity of California, San Diego, Deian StefanUniversity of California San Diego
Link to publication
11:00
30m
Talk
A Formal Analysis of Timing Channel Security via Bucketing
POST
Tachio TerauchiWaseda University, Timos AntonopoulosYale University
Link to publication
11:30
30m
Talk
A Dependently Typed Library for Static Information-Flow Control in Idris
POST
Simon Oddershede GregersenAarhus University, Søren Eller ThomsenAarhus University, Aslan AskarovAarhus University
Link to publication
12:00
30m
Talk
Achieving Safety Incrementally with Checked C
POST
Andrew Ruef, Leonidas LampropoulosUniversity of Pennsylvania, Ian Sweet, David Tarditi, Michael HicksUniversity of Maryland, College Park
Link to publication
14:00 - 16:00
Specification, Design, and Implementation of Particular Classes of SystemsFASE at JUPITER
Chair(s): Reiner HähnleTechnical University of Darmstadt
14:00
30m
Talk
CLTestCheck: Measuring Test Effectiveness for GPU Kernels
FASE
Chao PengUniversity of Edinburgh, UK, Ajitha RajanUniversity 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 BoerCentrum Wiskunde & Informatica, Leiden University, Einar Broch JohnsenUniversity of Oslo, Violet Ka I Pun, Silvia Lizeth Tapia TarifaUniversity of Oslo
Link to publication
15:00
30m
Talk
Optimal and Automated Deployment for Microservices
FASE
Mario BravettiUniversità di Bologna, Saverio GiallorenzoUniversity of Southern Denmark, Jacopo MauroUniversity 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 CleavelandUniversity 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 StoilkovskaVienna University of Technology , Igor KonnovInria Nancy, Josef WidderTU Wien, Florian ZulegerVienna University of Technology
Link to publication
15:00
30m
Talk
Measuring Masking Fault-Tolerance
TACAS
Pablo CastroDept. 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 SchubertHeinz Nixdorf Institut, Paderborn University, Ben HermannUniversity of Paderborn, Eric BoddenHeinz Nixdorf Institut, Paderborn University and Fraunhofer IEM
Link to publication
16:30 - 18:00
Software TestingFASE at JUPITER
Chair(s): Silvia Lizeth Tapia TarifaUniversity of Oslo
16:30
30m
Talk
CoVeriTest: Cooperative, Verifier-Based Testing
FASE
Dirk BeyerLMU Munich, Marie-Christine JakobsTU Darmstadt, Germany
Link to publication
17:00
30m
Talk
Pardis: Priority Aware Test Case Reduction
FASE
Golnaz Gharachorlu, Nick SumnerSimon Fraser University
Link to publication
17:30
30m
Talk
Automatically Identifying Sufficient Object Builders from Module APIs
FASE
Pablo PonzioDept. of Computer Science FCEFQyN, University of Rio Cuarto, Valeria BengoleaDept. of Computer Science FCEFQyN, University of Rio Cuarto, Mariano Politano, Nazareno AguirreDept. of Computer Science FCEFQyN, University of Rio Cuarto, Marcelo F. FriasDept. 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 BojanczykUniversity of Warsaw
16:30
30m
Talk
The Bernays-Schoenfinkel-Ramsey Class of Separation Logic on Arbitrary DomainsBest paper nomination
FOSSACS
Mnacho Echenim, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Nicolas Peltier
Link to publication