Program - ETAPS 2019

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 - 10:00
Talk

Invited Talk - "End-to-End Verification of Intelligent Cyber-Physical Systems: Progress and Challenges"

Nathan FultonMIT-IBM Watson AI Lab

10:00 - 10:10
Talk

Cross Programming Language Taint Analysis for the IoT Ecosystem

Pietro FerraraJuliaSoft SRL, Italy, Amit Kr MandalUniversità Ca' Foscari, Venezia, Italy, Agostino CortesiUniversità Ca' Foscari Venezia, Fausto SpotoU. Verona

10:10 - 10:20
Talk

FVL: Formal Verification in the Loop to Enhance Verification of Safety-Critical Cyber-Physical Systems

Cinzia BernardeshiUniv. of Pisa, Andrea DomeniciUniversity of Pisa, Italy, Sergio SaponaraUniversity of Pisa, Italy

10:20 - 10:30
Talk

Rigorous Design of FDIR Systems with BIP

Iulia Dragomir, Saddek BensalemVerimag

09:00 - 10:30: GaLoP - I at S3

09:00 - 10:00
Talk

Intertwining game theory and game semantics

Jules HedgesUniversity of Oxford

10:00 - 10:30
Talk

Universal property of the monad for infinite trace strategies (work in progress)

Paul Blain LevyUniversity of Birmingham, Sergey GoncharovFAU Erlangen-Nürnberg, Lehrstuhl 8, Lutz SchöderFAU Erlangen-Nürnberg, Lehrstuhl 8

09:00 - 10:30: DICE-FOPARA - I at S11
Chair(s): Steffen JostLMU, Munich, Germany

09:45 - 10:30
Talk

PRAMs over integers do not compute maxflow efficiently

Luc Pellissier, Thomas SeillerCNRS

09:00 - 10:30: HSB - I at S9
Chair(s): Milan CeskaBrno University of Technology

09:00 - 09:10
Day opening

Opening

09:10 - 10:10
Talk

Invited talk: Modelling and personalisation techniques for behavioural prediction and emotion recognition

Marta KwiatkowskaUniversity of Oxford

10:10 - 10:20
Short-paper

Poster flash: Comprehensive Modelling Platform

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 - 10:30
Short-paper

Poster flash: Formalizing metabolic-regulatory networks by hybrid automata

Lin LiuFreie Universität Berlin, Alexander BockmayrFreie Universität Berlin

09:00 - 10:30: BEHAPI - Mechanising Proofs for Behavioural Types and Processes at S4 (BEHAPI)
Chair(s): Antonio RavaraNOVA University of Lisbon and NOVA LINCS

09:00 - 09:30
Talk

A Theory of Contexts for Higher-Order Encodings of Process Algebras

Ivan ScagnettoUniversity of Udine

09:30 - 10:00
Talk

Formalising session-typed languages without worries

Wen KokkeUniversity of Edinburgh

10:00 - 10:30
Talk

Adventures in Formalising the Meta-Theory of Session Types

Francisco FerreiraImperial College London

09:00 - 10:00: Mooly Fest - Morning A at JUPITER

09:00 - 09:30
Talk

Calculational design of a static dependency analysis

Patrick Cousot

09:30 - 10:00
Talk

Automatic Detection of all Smart Contract Bugs

Mooly SagivTel Aviv University

09:00 - 10:30: TOOLympics - SV-COMP Talks at SW2 (TOOLympics)

09:00 - 10:30: TOOLympics - VerifyThis 1 (Opening and event presentation) at SU2

09:00 - 10:30: MeTRiD - Welcome & Keynote 1 at S510
Chair(s): Simon BliudzeINRIA Lillle - Nord Europe, Panagiotis KatsarosITI-CERTH, Thessaloniki

09:15 - 09:30
Day opening

Welcome

Simon BliudzeINRIA Lillle - Nord Europe, Panagiotis KatsarosITI-CERTH, Thessaloniki

09:30 - 10:30
Talk

The Role of Models as Digital Twins of Smart Processes, Machines and Parts in Industry 4.0

Tiziana MargariaUniversity of Limerick and Lero - The Irish Software Research Centre

10:30 - 12:00: Mooly Fest - Morning B at JUPITER

10:30 - 11:00
Talk

The Dilemma of Shape Analysis

Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.

11:00 - 11:30
Talk

Data Representation Synthesis: Past, Present and Future

Alex AikenStanford University

11:30 - 12:00
Talk

Mooly: Mensch, Marathon, Method, Magic

Thomas BallMicrosoft Research

10:30 - 16:00: Posters - Workshop Poster Exhibition (Saturday) at Coffee area (Posters)
Chair(s): Jan KofroňCharles University

10:30 - 10:52
Poster

Markovian equivalences for biochemical reaction networks

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 - 11:14
Poster

Statistical abstraction for multi-scale spatio-temporal systems

Michalis MichaelidesUniversity of Edinburgh, Jane HillstonUniversity of Edinburgh, Guido SanguinettiUniversity of Edinburgh

11:14 - 11:36
Poster

Towards Efficient Algorithms for Constraint Satisfaction Problems

Huu-Phuc VoUppsala University

11:36 - 11:58
Poster

VIAP 1.1

pritom rajkhowa, Fangzhen Lin

11:58 - 12:20
Poster

FreeST: context-free session types in a functional language

Bernardo AlmeidaUniversidade de Lisboa, Andreia MordidoLasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. VasconcelosUniversity of Lisbon, Portugal

12:20 - 12:42
Poster

WAPS: Weighted and Projected Sampling

Rahul Gupta, Shubham Sharma, Subhajit RoyIIT Kanpur, India, Kuldeep S. MeelNational University of Singapore

12:42 - 13:04
Poster

Semantic Fault Localization and Suspiciousness Ranking

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 - 13:26
Poster

Ultimate Automizer

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 - 13:48
Poster

CPAchecker with Strategy Selection

Karlheinz Friedberger, Marie-Christine JakobsTU Darmstadt, Germany, Thomas Lemberger, Martin Spießl, Philipp Wendler

13:48 - 14:10
Poster

Towards A Logical Account of Epistemic Causality

Shakil Khan, Mikhail Soutchanski

14:10 - 14:32
Poster

Minimal-Time Synthesis for Parametric Timed Automata

Étienne AndréLIPN, CNRS UMR 7030, Université Paris 13, Vincent BloemenUniversity of Twente, Laure PetrucciUniversité Paris 13, Jaco van de PolAarhus University

14:32 - 14:54
Poster

PeSCo: Predicting Sequential Combinations of Verifiers

Pavel Andrianov, Heike WehrheimPaderborn University

14:54 - 15:16
Poster

CoVeriTest: Cooperative Verifier-Based Testing

Dirk BeyerLMU Munich, Marie-Christine JakobsTU Darmstadt, Germany

15:16 - 15:38
Poster

JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)

Lucas CordeiroUniversity of Oxford, Daniel KroeningUniversity of Oxford, Peter SchrammelUniversity of Oxford, UK

15:38 - 16:00
Poster

CPALockator: Thread-Modular Approach with Transition Abstraction for Analysis of Multithreaded Software

Pavel Andrianov, Pavel Andrianov, Pavel Andrianov

11:00 - 12:00: LiVe - at S7

11:00 - 11:15
Talk

Industrial talk: Vahid Hashemi (AUDI): Industrial View on Safety of Learning

11:15 - 11:30
Talk

Marielle Stoelinga: Learning from failures: generating reliability models from data

11:30 - 11:45
Talk

Nathanaël Fijalkow: Data generation for programming by example

11:45 - 12:00
Talk

Nils Jansen: Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks

11:00 - 12:30: MeTRiD - Behavioural models and parametrised systems at S510
Chair(s): Tiziana MargariaUniversity of Limerick and Lero - The Irish Software Research Centre

11:00 - 11:40
Talk

Verification of Randomized Distributed Algorithms under Round-Rigid Adversaries

Nathalie BertrandINRIA Rennes, Igor KonnovInria Nancy, Marijana LazićTU Wien, Josef WidderTU Wien

11:40 - 12:20
Talk

Revisiting the Glue of BIP

Jacques CombazVerimag/CNRS

12:20 - 13:00
Talk

Programming Dynamic Reconfigurable Systems with DR-BIP

Rim El BallouliVerimag, Saddek BensalemVerimag, Marius BozgaVerimag/CNRS, Joseph SifakisVerimag/CNRS

11:00 - 12:30: PERR - II at S1 (PERR)

11:00 - 11:30
Talk

Understanding Counterexamples for Relational Properties with DIbugger

Mihai Herda, Michael KirstenKarlsruhe Institute of Technology (KIT), Etienne Brunner, Joana Plewnia, Ulla Scheler, Chiara Staudenmaier, Benedikt Wagner, Pascal Zwick, Bernhard BeckertKarlsruhe Institute of Technology

11:30 - 12:00
Talk

Analysis of program differences with numerical abstract interpretation

David DelmasAirbus & Sorbonne Université, Antoine MinéUPMC, France

Link to publication Pre-print File Attached

12:00 - 12:30
Talk

On Quantitative Comparison of Chemical Reaction Network Models

Ozan Kahramanogullari

11:00 - 12:00: InterAVT - II at S6

11:00 - 11:10
Talk

Advances in Usability of Formal Methods for Code Verification

Andre Maroneze, Valentin Perrelle, Florent Kirchner

11:10 - 11:20
Talk

Scalable Software Testing and Verification for Industrial-Scale Systems: The Challenges

Anila MjedaLero - The Irish Software Research Centre and University of Limerick, Goetz BotterweckLero - The Irish Software Research Centre and University of Limerick

11:20 - 11:30
Talk

AskTheCode: Interactive Call Graph Exploration for Error Fixing and Prevention

Robert Husak, Jan KofroňCharles University, Filip Zavoral

11:30 - 12:00
Talk

Lighting talks (non-authors)

11:00 - 12:00: GaLoP - II at S3

11:00 - 11:30
Talk

Characterizing Downwards Closed Strongly First Order Dependencies

Pietro GallianiFree University of Bozen-Bolzano

11:30 - 12:00
Talk

Logics for first-order definable team properties

Juha Kontinen, Fan YangUniversity of Helsinki

11:00 - 12:00: DICE-FOPARA - II at S11
Chair(s): Steffen JostLMU, Munich, Germany

11:00 - 11:45
Talk

Towards a Sheaf-Theoretic Definition of Decision Problems

Damiano MazzaCNRS

11:00 - 12:00: BEHAPI - Mechanising Proofs of Behavioural Types for APIs at S4 (BEHAPI)
Chair(s): Luca PadovaniUniversity of Turin

11:00 - 11:20
Talk

Proving properties about Linear Pi in Coq

Antonio RavaraNOVA University of Lisbon and NOVA LINCS, Marco GiuntiNOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa

11:20 - 11:40
Talk

Binary Session Types in Coq

Ornela DardhaUniversity of Glasgow

11:40 - 12:00
Talk

Mechanise your proofs in Coq: From zero to cut-admissibility in less than three months.

Marco CarboneIT University of Copenhagen

11:00 - 12:30: HSB - Modelling at S9
Chair(s): Tatjana PetrovUniversität Konstanz

11:00 - 11:30
Talk

A Hybrid HMM Approach for the Dynamics of DNA Methylation

Charalampos KyriakopoulosSaarland University, Pascal GiehrSaarland University, Alexander LückSaarland University, Jörn WalterSaarland University, Verena WolfSaarland University

11:30 - 12:00
Talk

Controlling noisy expression through auto regulation of burst frequency and protein stability

Pavol BokesComenius University, Abhyudai SinghUniversity of Delaware

12:00 - 12:30
Talk

Using a hybrid approach to model central carbon metabolism across the cell cycle

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: TOOLympics - SL-COMP at S5

11:00 - 12:30: TOOLympics - SV-COMP Meeting at SW2 (TOOLympics)

11:00 - 12:00: SynCoP - Timed systems at S10

11:00 - 11:45
Talk

On Parameterised Jobshop Scheduling Problems

Peter HabermehlIRIF

11:00 - 12:30: TOOLympics - VerifyThis 2 (Verification challenge 1) at SU2

13:30 - 15:30: LiVe - at S7

13:30 - 14:30
Talk

Invited talk: Kristian Kersting: Exploiting Symmetries for Modelling and Solving Quadratic Programs

14:30 - 15:30
Talk

Daniel Neider: Horn-ICE Learning

13:30 - 15:30: SynCoP - Applications at S10

13:45 - 14:30
Talk

Parametric statistical model checking of UAV flightplan

Ran Bao, Christian Attiogbe, Benoit Delahaye

14:30 - 15:15
Talk

Fault-tolerant matrix factorisation: a formal model and proof

Camille CotiLIPN, Université Paris 13, Laure PetrucciUniversité Paris 13, Daniel Alberto Torres GonzalezLIPN, Université Paris 13

13:30 - 15:30: BEHAPI - Behavioural Types for API-based software at S4 (BEHAPI)
Chair(s): emilio tuostoUniversity of Leicester

13:30 - 14:00
Talk

Mailbox Types for Unordered Interactions

Ugo de'LiguoroUniversità di Torino, Luca PadovaniUniversity of Turin

14:00 - 14:30
Talk

A Behavioural Type System for Mungo with Generics

Hans HüttelDepartment of Computer Science, Aalborg University

14:30 - 15:00
Talk

A Virtual-Machine Metaobject Protocol for Run-Time Software Adaptation

Guido ChariCzech Technical University, Czechia

15:00 - 15:30
Talk

Hardware Interactions as Behavioural Types.

Francisco MartinsUniversity of Lisbon

13:30 - 15:30: InterAVT - III at S6

13:30 - 15:30
Meeting

Speed-dating

13:30 - 15:30: GaLoP - III at S3

13:30 - 14:30
Talk

Model checking games: the recent advances on parity games

Nathanaël FijalkowCNRS, LaBRI, and Alan Turing Institute

14:30 - 15:00
Talk

A Framework for Compositional Model Checking

Yu-Yang LinQueen Mary University of London, Nikos TzevelekosQueen Mary University of London

15:00 - 15:30
Talk

Modalities as prices: a game model of intuitionistic linear logic with subexponentials

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: DICE-FOPARA - III at S11
Chair(s): Patrick BaillotCNRS & ENS Lyon

14:00 - 14:45
Talk

Type-two Iteration with Bounded Query Revision

Bruce KapronUniversity of Victoria, Florian SteinbergINRIA Saclay

14:45 - 15:30
Talk

Tiered complexity at higher order

Emmanuel Hainry, Bruce KapronUniversity of Victoria, Jean-Yves Marion LORIA, Romain PéchouxINRIA / LORIA

14:00 - 15:30: Mooly Fest - Afternoon A at JUPITER

14:00 - 14:30
Talk

Proofs and Counterexamples

Neil ImmermanUniversity of Massachusetts, Amherst

14:30 - 15:00
Talk

Concurrency Control Contract Composition

G. RamalingamMicrosoft Research

15:00 - 15:30
Talk

Special Relations for Special Relationships

Nikolaj BjørnerMicrosoft Research

14:00 - 15:30: PERR - III at S1 (PERR)

14:00 - 15:00
Talk

Invited talk by Marco Eilers

Marco EilersETH Zurich

15:00 - 15:30
Talk

Relational Verification via Invariant-Guided Synchronization

Qi Zhou, David Heath, William Harris

14:00 - 15:30: MeTRiD - Keynote 2 at S510
Chair(s): Panagiotis KatsarosITI-CERTH, Thessaloniki

14:30 - 15:30
Talk

Cyber-Physical Components as building blocks of more dependable industrial CPS

Valeriy VyatkinAalto University, Finland and Luleå University of Technology, Sweden

14:00 - 15:30: HSB - Oded Maler memorial (1) at S9
Chair(s): Nicola PaolettiRoyal Holloway, University of London, UK

14:00 - 15:00
Talk

Oded Maler: An odyssey from Computer Science to Biological Sciences

Thao DangCNRS/VERIMAG

14:00 - 15:30: TOOLympics - RERS 1 at S5

14:00 - 15:30: TOOLympics - Test-Comp Talks at SW2 (TOOLympics)

14:00 - 15:30: TOOLympics - VerifyThis 3 (Verification challenge 3) at SU2

16:00 - 18:00: LiVe - at S7

16:00 - 16:20
Talk

Stefan Ratschan: Learning Certificates

16:20 - 16:40
Talk

Yutaka Nagashima: Towards Machine Learning Induction

16:40 - 17:00
Talk

Maximilian Weininger: BRTDP for Stochastic Games

16:00 - 17:00: Mooly Fest - Afternoon B at JUPITER

16:00 - 16:30
Talk

Decidable Reasoning for Verification: How Far Can You EPR?

Oded PadonStanford University

16:30 - 17:00
Talk

code2seq: Generating Sequences from Structured Representations of Code

Eran YahavTechnion

16:00 - 18:00: BEHAPI - BehAPI Business Meeting at S4 (BEHAPI)
Chair(s): Adrian FrancalanzaUniversity of Malta

16:00 - 17:00
Talk

BehAPI Practices

Caroline CaruanaUniversity of Malta

17:00 - 18:00
Meeting

BehAPI Year 1 Review and Year 2 projections

Adrian FrancalanzaUniversity of Malta

16:00 - 18:00: MeTRiD - Cyber-Physical Systems design at S510
Chair(s): Valeriy VyatkinAalto University, Finland and Luleå University of Technology, Sweden

16:00 - 16:40
Talk

Localizing Faults in Simulink/Stateflow Models with STL

Ezio BartocciTechnische Universität Wien, Thomas FerrèreIST Austria, Niveditha ManjunathAustrian Institute of Technology, Dejan NickovicAustrian Institute of Technology

16:40 - 17:20
Talk

Model-based energy characterization of IoT system design aspects

Alexios LekidisAristotle University of Thessaloniki

17:20 - 18:00
Talk

Modeling and Simulation of Attacks on Cyber-physical Systems

Cinzia BernardeshiUniv. of Pisa

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

16:00 - 16:30
Talk

Automatic Equivalence Proofs for Programs with Algebraic Data Types

Moritz Kiefer, Mattias UlbrichKarlsruhe Institute of Technology

16:30 - 17:00
Talk

Proving Program Equivalence with Constrained Rewriting Induction and Ctrl

Carsten FuhsBirkbeck, University of London, Cynthia KopRadboud University Nijmegen, Naoki NishidaNagoya University

17:00 - 17:30
Talk

Semantics-Based Proofs of Equivalence for Functions with Accumulators

Stefan CiobacaAlexandru Ioan Cuza University of Iasi, Dorel Lucanu, Sebastian Buruiana

16:00 - 18:00: InterAVT - IV at S6

16:00 - 17:15
Meeting

Collaboration Session

17:15 - 17:30
Talk

Wrap-up

16:00 - 18:00: GaLoP - IV at S3

16:00 - 16:30
Talk

Sequential algorithms and innocent strategies share the same execution mechanism

Pierre-Louis CurienUniv. Paris Diderot and INRIA Paris-Rocquencourt

16:30 - 17:10
Talk

A Dialectica-Like Interpretation of a Linear MSO on Infinite Words

Colin Riba, Pierre Pradic

16:00 - 18:00: DICE-FOPARA - IV at S11
Chair(s): Damiano MazzaCNRS

16:00 - 16:45
Talk

Pointers in Recursion: Exploring the Tropics

Paulin Jacobé De Naurois

16:45 - 17:30
Talk

Hierarchical Digging is EXPTIME

Brian Redmond

16:00 - 18:00: SynCoP - Markov decision processes at S10

16:00 - 16:45
Talk

Convex Optimization meets Parameter Synthesis for MDPs

Nils Jansen

16:45 - 17:30
Talk

Learning-Based Mean-Payoff Optimization in an unknown MDP under Omega-Regular Constraints

Jan KretinskyTechnical University of Munich

16:00 - 18:00: HSB - Oded Maler memorial (2) at S9
Chair(s): Nicola PaolettiRoyal Holloway, University of London, UK

16:00 - 17:00
Talk

From Sensitive to Formal Barbaric Systems Biology

Alexandre DonzeUniversity of California, Berkeley

17:00 - 18:00
Talk

Timed Patterns: from Definition to Matching and Monitoring, a survey in memoriam Oded Maler

Eugene AsarinIRIF, University Paris Diderot and CNRS, France

16:00 - 18:00: TOOLympics - RERS 2 at S5

16:00 - 18:00: TOOLympics - Test-Comp Meeting at SW2 (TOOLympics)

16:00 - 18:00: TOOLympics - VerifyThis 4 (Verification challenge 3) at SU2

Sun 7 Apr

08:00 - 09:00: Mentoring Workshop - Mentoring Breakfast I at JUPITER

09:00 - 10:30: CREST - Actual causation at S6

09:00 - 09:45
Talk

Probabilistic Actual Causation

Luke Fenton-GlynnUniversity College London

File Attached

09:45 - 10:10
Research paper

Causality & Control flow [Robert Kunnemann, Deepak Garg, Michael Backes]

File Attached

10:10 - 10:30
Research paper

Extending Causal Models from Machines into Humans [Severin Kacianka, Amjad Ibrahim, Alexander Pretschner, Alexander Trende, Andreas Ludtke]

File Attached

09:00 - 10:30: HCVS - I at S4 (HCVS)
Chair(s): Maurizio ProiettiCNR-IASI

09:00 - 10:00

Invited Talk: Concolic testing of higher-order functional languages

Konstantinos (Kostis) SagonasUppsala University

File Attached

10:00 - 10:30
Talk

HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories

C.-H. Luke OngUniversity of Oxford, Dominik Wagner

Pre-print File Attached

09:00 - 10:30: TOOLympics - MCC at S5

09:00 - 10:00: Mentoring Workshop - Morning Session I at Mentoring

09:00 - 10:00
Talk

From Shape Analysis to Smart Contract Verification: A journey in proof automationKeynote

Mooly SagivTel Aviv University

File Attached

09:00 - 10:30: SynCoP - Parameter synthesis for LTL at S10

09:00 - 09:45
Talk

Parameter Synthesis for Timed Automata with Clock-Aware LTL Properties

Nikola Benes

09:45 - 10:30
Talk

Pruning NDFS for Parametric Timed Automata

Laure PetrucciUniversité Paris 13, Jaco van de PolAarhus University

09:00 - 10:30: SYNT Camp - Reactive Synthesis Background & SYNTCOMP at SW2 (SYNT Camp)
Chair(s): Guillermo A. PerezUniversity of Antwerp, Leander TentrupSaarland University

09:00 - 10:00
Tutorial

Reactive Synthesis Background and the Synthesis Competition

Guillermo A. PerezUniversity of Antwerp

10:00 - 10:30
Tutorial

Hand-on Synthesis Experience with BoSy

Leander TentrupSaarland University

Link to publication DOI Pre-print

09:00 - 10:30: PLACES - Session 1 at S8
Chair(s): Francisco MartinsUniversity of Lisbon

09:00 - 10:00
Talk

Keynote: Unstructured Parallelism Considered Harmful -- Using Structured Parallelism for Enhanced Software Verification

Vivek SarkarRice University, USA

10:00 - 10:30
Full-paper

A Message-Passing Interpretation of Adjoint Logic

Klaas PruiksmaCarnegie Mellon University, Frank PfenningCarnegie Mellon University, USA

09:00 - 10:30: QAPL - Session I at S7

09:00 - 10:00
Talk

Principles of QAPL: What I learned in nearly 20 years and what I still don’t understand

Herbert WiklickyImperial College London

10:00 - 10:30
Talk

Probabilistic output analyses for deterministic programs -reusing existing non-probabilistic analyses

Maja KirkebyRoskilde University

Pre-print

09:00 - 10:30: GaLoP - V at S3

09:00 - 10:00
Talk

Template games: a homotopy model of differential linear logic

Paul-André MelliesCNRS and University Paris Diderot

10:00 - 10:30
Talk

Simple game semantics and Day convolution

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: DICE-FOPARA - V at S11
Chair(s): Thomas SeillerCNRS

09:00 - 09:45
Talk

Finite semantics of polymorphism, complexity and the power of type fixpoints

Lê Thành Dũng Nguyễn, Thomas SeillerCNRS, Paolo PistoneUniversity of Tübingen, Lorenzo Tortora de Falco

09:45 - 10:30
Talk

From normal functors to logarithmic space queries

Lê Thành Dũng Nguyễn, Pierre Pradic

09:00 - 10:30: HSB - V at S9
Chair(s): Nicola PaolettiRoyal Holloway, University of London, UK

09:00 - 10:00
Talk

Invited talk: Closed-loop neurohybrid interfaces: from in vitro to in vivo studies and beyond

Michela ChiappaloneItalian Institute of Technology

10:00 - 10:30
Talk

Temporal Logic Based Synthesis of Experimentally Constrained Interaction Networks

Judah GoldfederYeshiva University, Hillel KuglerMicrosoft

09:00 - 10:30: TOOLympics - VerifyThis 5 (Judging and team presentations 1) at SU2

10:30 - 12:00: Mentoring Workshop - Morning Session II at Mentoring

10:30 - 11:00
Talk

How to Give an Effective Talk

Ajitha RajanUniversity of Edinburgh

11:00 - 11:30
Talk

Navigating through the academic jungle: tips, tricks & traps

Marielle StoelingaUniversity of Twente and Radboud University, Nijmegen

11:30 - 12:00
Talk

Push, Pull, Partner - A Few Models for Industrial Research

Thomas BallMicrosoft Research

10:30 - 16:00: Posters - Workshop Poster Exhibition (Sunday) at Coffee area (Posters)

10:30 - 10:52
Poster

CPALockator: Thread-Modular Approach with Transition Abstraction for Analysis of Multithreaded Software

Pavel Andrianov, Pavel Andrianov, Pavel Andrianov

10:52 - 11:14
Poster

CPAchecker with Strategy Selection

Karlheinz Friedberger, Marie-Christine JakobsTU Darmstadt, Germany, Thomas Lemberger, Martin Spießl, Philipp Wendler

11:14 - 11:36
Poster

CoVeriTest: Cooperative Verifier-Based Testing

Dirk BeyerLMU Munich, Marie-Christine JakobsTU Darmstadt, Germany

11:36 - 11:58
Poster

FreeST: context-free session types in a functional language

Bernardo AlmeidaUniversidade de Lisboa, Andreia MordidoLasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. VasconcelosUniversity of Lisbon, Portugal

11:58 - 12:20
Poster

JBMC: Bounded Model Checking for Java Bytecode (Competition Contribution)

Lucas CordeiroUniversity of Oxford, Daniel KroeningUniversity of Oxford, Peter SchrammelUniversity of Oxford, UK

12:20 - 12:42
Poster

Markovian equivalences for biochemical reaction networks

12:42 - 13:04
Poster

Minimal-Time Synthesis for Parametric Timed Automata

Étienne AndréLIPN, CNRS UMR 7030, Université Paris 13, Vincent BloemenUniversity of Twente, Laure PetrucciUniversité Paris 13, Jaco van de PolAarhus University

13:04 - 13:26
Poster

PeSCo: Predicting Sequential Combinations of Verifiers

Pavel Andrianov, Heike WehrheimPaderborn University

13:26 - 13:48
Poster

Semantic Fault Localization and Suspiciousness Ranking

13:48 - 14:10
Poster

Statistical abstraction for multi-scale spatio-temporal systems

Michalis MichaelidesUniversity of Edinburgh, Jane HillstonUniversity of Edinburgh, Guido SanguinettiUniversity of Edinburgh

14:10 - 14:32
Poster

Towards A Logical Account of Epistemic Causality

Shakil Khan, Mikhail Soutchanski

14:32 - 14:54
Poster

Towards Efficient Algorithms for Constraint Satisfaction Problems

Huu-Phuc VoUppsala University

14:54 - 15:16
Poster

Ultimate Automizer

15:16 - 15:38
Poster

VIAP 1.1

pritom rajkhowa, Fangzhen Lin

15:38 - 16:00
Poster

WAPS: Weighted and Projected Sampling

Rahul Gupta, Shubham Sharma, Subhajit RoyIIT Kanpur, India, Kuldeep S. MeelNational University of Singapore

11:00 - 12:30: HSB - Analysis at S9
Chair(s): Jerome FeretINRIA Paris

11:00 - 11:30
Talk

Fixed-point Computation of Equilibria in Biochemical Regulatory Networks

11:30 - 12:00
Talk

Rejection-Based Simulation of Stochastic Spreading Processes on Complex Networks

Gerrit GroßmannSaarland University, Verena WolfSaarland University

12:00 - 12:30
Talk

rPrism -- A software for reactive weighted state transition models

Daniel FigueiredoUniversity of Aveiro, Eugénio A. M. RochaUniversity of Aveiro, Madalena ChavesINRIA, Manuel A. MartinsUniversity of Aveiro

11:00 - 12:30: CREST - Causal discovery methods at S6

11:00 - 11:45
Talk

Computational Causal Discovery and its Applications

Sisi MaUniversity of Minnesota

File Attached

11:45 - 12:30
Talk

Towards a Science of Perspicuous Computing - Lessons learnt from the Analysis of Automotive Emissions Control Systems

Holger HermannsSaarland University

File Attached

11:00 - 12:00: SYNT Camp - Hands-on BoSy Tutorial at SW2 (SYNT Camp)
Chair(s): Guillermo A. PerezUniversity of Antwerp, Leander TentrupSaarland University

11:00 - 12:00
Tutorial

Hand-on Synthesis Experience with BoSy (part 2)

Leander TentrupSaarland University

11:00 - 12:30: SPIoT - I at S510

11:00 - 11:30

Invited Talk: Expected Cost Analysis of Attack-Defence Trees

Jan KretinskyTechnical University of Munich

11:30 - 12:00
Talk

Static Analysis for the OWASP IoT Top 10 2018.

Pietro FerraraJuliaSoft SRL, Italy, Amit Kr MandalUniversità Ca' Foscari, Venezia, Italy, Agostino CortesiUniversità Ca' Foscari Venezia, Fausto SpotoU. Verona

12:00 - 12:30
Talk

The Refinement-Risk Loop - A Process for Security Engineering in Isabelle

Florian KammüllerMiddlesex University, UK

11:00 - 12:00: PLACES - II at S8
Chair(s): Ornela DardhaUniversity of Glasgow

11:00 - 11:30
Full-paper

FreeST: context-free session types in a functional language

Bernardo AlmeidaUniversidade de Lisboa, Andreia MordidoLasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. VasconcelosUniversity of Lisbon, Portugal

11:30 - 12:00
Full-paper

Concurrent Typestate-Oriented Programming in Java

Rosita GerboUniversità di Torino, Luca PadovaniUniversity of Turin

11:00 - 12:00: HCVS - II at S4 (HCVS)
Chair(s): Mattias UlbrichKarlsruhe Institute of Technology

11:00 - 11:30
Talk

Challenges in the specialisation of smart Horn clause interpreters

John P. GallagherRoskilde University

File Attached

11:30 - 12:00
Full-paper

Proving Properties of Sorting Programs: A Case Study in Horn Clause Verification

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:00: SynCoP - SMT at S10

11:00 - 11:45
Talk

SMT-based bounded model checking for parametric reaction systems

Wojciech PenczekIPI-PAN, Artur Meski

11:00 - 12:30: QAPL - Session II at S7

11:00 - 11:30
Talk

A Faster-Than Relation for Semi-Markov Decision Processes

Mathias Ruggaard PedersenAalborg University, Giorgio BacciAalborg University, Kim LarsenAalborg University

Pre-print

11:30 - 12:00
Talk

Automatic Synthesis of Polynomial Probabilistic Invariants via Geometric Persistence