ETAPS 2019 (series) /
ETAPS 2019 Program
Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sat 6 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sat 6 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 30mTalk | Calculational design of a static dependency analysis Mooly Fest | ||
09:30 30mTalk | Automatic Detection of all Smart Contract Bugs Mooly Fest Mooly Sagiv Tel Aviv University | ||
09:00 - 10:30 | |||
09:00 60mTalk | Invited talk by Margus Veanes PERR Margus Veanes Microsoft Research | ||
10:00 30mTalk | 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 | |||
09:45 45mTalk | PRAMs over integers do not compute maxflow efficiently DICE-FOPARA | ||
09:00 - 10:30 | |||
09:00 60mTalk | Intertwining game theory and game semantics GaLoP | ||
10:00 30mTalk | 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 30mTalk | A Theory of Contexts for Higher-Order Encodings of Process Algebras BEHAPI Ivan Scagnetto University of Udine | ||
09:30 30mTalk | Formalising session-typed languages without worries BEHAPI Wen Kokke University of Edinburgh | ||
10:00 30mTalk | Adventures in Formalising the Meta-Theory of Session Types BEHAPI Francisco Ferreira Imperial College London | ||
09:00 - 10:30 | |||
09:00 - 10:30 | Welcome & Keynote 1MeTRiD at S510 Chair(s): Simon Bliudze INRIA Lillle - Nord Europe, Panagiotis Katsaros ITI-CERTH, Thessaloniki | ||
09:15 15mDay opening | Welcome MeTRiD | ||
09:30 60mTalk | The Role of Models as Digital Twins of Smart Processes, Machines and Parts in Industry 4.0 MeTRiD Tiziana Margaria University of Limerick and Lero - The Irish Software Research Centre | ||
09:00 - 10:30 | |||
09:00 30mTalk | 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 30mTalk | Invited Talk - "End-to-End Verification of Intelligent Cyber-Physical Systems: Progress and Challenges" InterAVT Nathan Fulton MIT-IBM Watson AI Lab | ||
10:00 10mTalk | 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 10mTalk | 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 10mTalk | Rigorous Design of FDIR Systems with BIP InterAVT | ||
09:00 - 10:30 | |||
09:00 5mTalk | Opening LiVe | ||
09:05 55mTalk | Invited talk: Bettina Könighofer: Safe and Optimized Learning via Shielding LiVe | ||
10:00 30mTalk | Industrial talk: Martin Neuhäußer (Siemens): Verifying the approximate: Challenges in neural network analysis LiVe | ||
09:00 - 10:30 | |||
09:00 10mDay opening | Opening HSB | ||
09:10 60mTalk | Invited talk: Modelling and personalisation techniques for behavioural prediction and emotion recognition HSB Marta Kwiatkowska University of Oxford | ||
10:10 10mShort-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 10mShort-paper | Poster flash: Formalizing metabolic-regulatory networks by hybrid automata HSB | ||
09:00 - 10:30 | |||
09:00 - 10:30 | |||
10:30 - 12:00 | |||
10:30 30mTalk | The Dilemma of Shape Analysis Mooly Fest Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc. | ||
11:00 30mTalk | Data Representation Synthesis: Past, Present and Future Mooly Fest Alex Aiken Stanford University | ||
11:30 30mTalk | Mooly: Mensch, Marathon, Method, Magic Mooly Fest Thomas Ball Microsoft Research | ||
11:00 - 12:30 | |||
11:00 30mTalk | 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 30mTalk | Analysis of program differences with numerical abstract interpretation PERR Link to publication Pre-print File Attached | ||
12:00 30mTalk | On Quantitative Comparison of Chemical Reaction Network Models PERR | ||
11:00 - 12:00 | |||
11:00 45mTalk | On Parameterised Jobshop Scheduling Problems SynCoP Peter Habermehl IRIF | ||
11:00 - 12:00 | |||
11:00 45mTalk | Towards a Sheaf-Theoretic Definition of Decision Problems DICE-FOPARA Damiano Mazza CNRS | ||
11:00 - 12:00 | |||
11:00 30mTalk | Characterizing Downwards Closed Strongly First Order Dependencies GaLoP Pietro Galliani Free University of Bozen-Bolzano | ||
11:30 30mTalk | Logics for first-order definable team properties GaLoP | ||
11:00 - 12:00 | Mechanising Proofs of Behavioural Types for APIsBEHAPI at S4 (BEHAPI) Chair(s): Luca Padovani University of Turin | ||
11:00 20mTalk | 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 20mTalk | Binary Session Types in Coq BEHAPI Ornela Dardha University of Glasgow | ||
11:40 20mTalk | 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 | |||
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 40mTalk | 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 40mTalk | Revisiting the Glue of BIP MeTRiD Jacques Combaz Verimag/CNRS | ||
12:20 40mTalk | Programming Dynamic Reconfigurable Systems with DR-BIP MeTRiD Rim El Ballouli Verimag, Saddek Bensalem Verimag, Marius Bozga Verimag/CNRS, Joseph Sifakis Verimag/CNRS | ||
11:00 - 12:00 | |||
11:00 10mTalk | Advances in Usability of Formal Methods for Code Verification InterAVT | ||
11:10 10mTalk | 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 10mTalk | AskTheCode: Interactive Call Graph Exploration for Error Fixing and Prevention InterAVT | ||
11:30 30mTalk | Lighting talks (non-authors) InterAVT | ||
11:00 - 12:30 | |||
11:00 30mTalk | 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 30mTalk | Controlling noisy expression through auto regulation of burst frequency and protein stability HSB | ||
12:00 30mTalk | 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 | |||
11:00 - 12:30 | |||
13:30 - 15:30 | |||
13:45 45mTalk | Parametric statistical model checking of UAV flightplan SynCoP | ||
14:30 45mTalk | 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 | |||
14:00 45mTalk | Type-two Iteration with Bounded Query Revision DICE-FOPARA | ||
14:45 45mTalk | 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 | |||
13:30 60mTalk | Model checking games: the recent advances on parity games GaLoP | ||
14:30 30mTalk | A Framework for Compositional Model Checking GaLoP | ||
15:00 30mTalk | 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 30mTalk | Mailbox Types for Unordered Interactions BEHAPI | ||
14:00 30mTalk | A Behavioural Type System for Mungo with Generics BEHAPI | ||
14:30 30mTalk | A Virtual-Machine Metaobject Protocol for Run-Time Software Adaptation BEHAPI Guido Chari Czech Technical University, Czechia | ||
15:00 30mTalk | Hardware Interactions as Behavioural Types. BEHAPI Francisco Martins University of Lisbon | ||
13:30 - 15:30 | |||
13:30 2hMeeting | Speed-dating InterAVT | ||
13:30 - 15:30 | |||
13:30 60mTalk | Invited talk: Kristian Kersting: Exploiting Symmetries for Modelling and Solving Quadratic Programs LiVe | ||
14:30 60mTalk | Daniel Neider: Horn-ICE Learning LiVe | ||
14:00 - 15:30 | |||
14:00 30mTalk | Proofs and Counterexamples Mooly Fest Neil Immerman University of Massachusetts, Amherst | ||
14:30 30mTalk | Concurrency Control Contract Composition Mooly Fest G. Ramalingam Microsoft Research | ||
15:00 30mTalk | Special Relations for Special Relationships Mooly Fest Nikolaj Bjørner Microsoft Research | ||
14:00 - 15:30 | |||
14:00 60mTalk | Invited talk by Marco Eilers PERR Marco Eilers ETH Zurich | ||
15:00 30mTalk | Relational Verification via Invariant-Guided Synchronization PERR | ||
14:00 - 15:30 | |||
14:00 - 15:30 | |||
14:30 60mTalk | 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 | |||
14:00 60mTalk | Oded Maler: An odyssey from Computer Science to Biological Sciences HSB Thao Dang CNRS/VERIMAG | ||
14:00 - 15:30 | |||
14:00 - 15:30 | |||
16:00 - 17:00 | |||
16:00 30mTalk | Decidable Reasoning for Verification: How Far Can You EPR? Mooly Fest Oded Padon Stanford University | ||
16:30 30mTalk | code2seq: Generating Sequences from Structured Representations of Code Mooly Fest Eran Yahav Technion | ||
16:00 - 18:00 | |||
16:00 30mTalk | Automatic Equivalence Proofs for Programs with Algebraic Data Types PERR | ||
16:30 30mTalk | 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 30mTalk | Semantics-Based Proofs of Equivalence for Functions with Accumulators PERR | ||
16:00 - 18:00 | |||
16:00 45mTalk | Convex Optimization meets Parameter Synthesis for MDPs SynCoP | ||
16:45 45mTalk | Learning-Based Mean-Payoff Optimization in an unknown MDP under Omega-Regular Constraints SynCoP Jan Kretinsky Technical University of Munich | ||
16:00 - 18:00 | |||
16:00 45mTalk | Pointers in Recursion: Exploring the Tropics DICE-FOPARA | ||
16:45 45mTalk | Hierarchical Digging is EXPTIME DICE-FOPARA | ||
16:00 - 18:00 | |||
16:00 30mTalk | Sequential algorithms and innocent strategies share the same execution mechanism GaLoP Pierre-Louis Curien Univ. Paris Diderot and INRIA Paris-Rocquencourt | ||
16:30 40mTalk | A Dialectica-Like Interpretation of a Linear MSO on Infinite Words GaLoP | ||
16:00 - 18:00 | |||
16:00 60mTalk | BehAPI Practices BEHAPI Caroline Caruana University of Malta | ||
17:00 60mMeeting | BehAPI Year 1 Review and Year 2 projections BEHAPI Adrian Francalanza University of Malta | ||
16:00 - 18:00 | |||
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 40mTalk | 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 40mTalk | Model-based energy characterization of IoT system design aspects MeTRiD Alexios Lekidis Aristotle University of Thessaloniki | ||
17:20 40mTalk | Modeling and Simulation of Attacks on Cyber-physical Systems MeTRiD Cinzia Bernardeshi Univ. of Pisa | ||
16:00 - 18:00 | |||
16:00 75mMeeting | Collaboration Session InterAVT | ||
17:15 15mTalk | Wrap-up InterAVT | ||
16:00 - 18:00 | |||
16:00 20mTalk | Stefan Ratschan: Learning Certificates LiVe | ||
16:20 20mTalk | Yutaka Nagashima: Towards Machine Learning Induction LiVe | ||
16:40 20mTalk | Maximilian Weininger: BRTDP for Stochastic Games LiVe | ||
16:00 - 18:00 | |||
16:00 60mTalk | From Sensitive to Formal Barbaric Systems Biology HSB Alexandre Donze University of California, Berkeley | ||
17:00 60mTalk | 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 | |||
16:00 - 18:00 | |||
Sun 7 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 7 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
08:00 - 09:00 | |||
09:00 - 10:00 | |||
09:00 60mTalk | 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 | |||
09:00 45mTalk | Parameter Synthesis for Timed Automata with Clock-Aware LTL Properties SynCoP | ||
09:45 45mTalk | Pruning NDFS for Parametric Timed Automata SynCoP | ||
09:00 - 10:30 | |||
09:00 45mTalk | 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 45mTalk | From normal functors to logarithmic space queries DICE-FOPARA | ||
09:00 - 10:30 | |||
09:00 60mTalk | Template games: a homotopy model of differential linear logic GaLoP | ||
10:00 30mTalk | Simple game semantics and Day convolution GaLoP Clovis Eberhart National Institute of Informatics, Japan, Tom Hirschowitz Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry, Alexis Laouar Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS | ||
09:00 - 10:30 | |||
09:00 60m | Invited Talk: Concolic testing of higher-order functional languages HCVS Konstantinos (Kostis) Sagonas Uppsala University File Attached | ||
10:00 30mTalk | HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories HCVS Pre-print File Attached | ||
09:00 - 10:30 | |||
09:00 - 10:30 | |||
09:00 45mTalk | Probabilistic Actual Causation CREST Luke Fenton-Glynn University College London File Attached | ||
09:45 25mResearch paper | Causality & Control flow [Robert Kunnemann, Deepak Garg, Michael Backes] CREST File Attached | ||
10:10 20mResearch 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 | |||
09:00 60mTalk | 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 30mTalk | Probabilistic output analyses for deterministic programs -reusing existing non-probabilistic analyses QAPL Maja Kirkeby Roskilde University Pre-print | ||
09:00 - 10:30 | |||
09:00 60mTalk | Keynote: Unstructured Parallelism Considered Harmful -- Using Structured Parallelism for Enhanced Software Verification PLACES Vivek Sarkar Rice University, USA | ||
10:00 30mFull-paper | A Message-Passing Interpretation of Adjoint Logic PLACES | ||
09:00 - 10:30 | |||
09:00 60mTalk | Invited talk: Closed-loop neurohybrid interfaces: from in vitro to in vivo studies and beyond HSB Michela Chiappalone Italian Institute of Technology | ||
10:00 30mTalk | Temporal Logic Based Synthesis of Experimentally Constrained Interaction Networks HSB | ||
09:00 - 10:30 | |||
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 60mTutorial | Reactive Synthesis Background and the Synthesis Competition SYNT Camp Guillermo A. Perez University of Antwerp | ||
10:00 30mTutorial | Hand-on Synthesis Experience with BoSy SYNT Camp Leander Tentrup Saarland University Link to publication DOI Pre-print | ||
10:30 - 12:00 | |||
10:30 30mTalk | How to Give an Effective Talk Mentoring Workshop Ajitha Rajan University of Edinburgh | ||
11:00 30mTalk | Navigating through the academic jungle: tips, tricks & traps Mentoring Workshop Marielle Stoelinga University of Twente and Radboud University, Nijmegen | ||
11:30 30mTalk | Push, Pull, Partner - A Few Models for Industrial Research Mentoring Workshop Thomas Ball Microsoft Research | ||
11:00 - 12:00 | |||
11:00 45mTalk | SMT-based bounded model checking for parametric reaction systems SynCoP | ||
11:00 - 12:00 | |||
11:00 60mTalk | (Invited Talk) Cons-free Rewriting DICE-FOPARA Cynthia Kop Radboud University Nijmegen | ||
11:00 - 12:00 | |||
11:00 30mTalk | A game semantics understanding of asynchronous multiparty session types subtyping GaLoP | ||
11:30 30mTalk | Probabilistic Programming Inference via Intensional Semantics GaLoP | ||
11:00 - 12:00 | |||
11:00 30mTalk | Challenges in the specialisation of smart Horn clause interpreters HCVS John P. Gallagher Roskilde University File Attached | ||
11:30 30mFull-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 | |||
11:00 11mMeeting | CHC-COMP TOOLympics | ||
11:11 11mMeeting | QComp TOOLympics | ||
11:22 11mMeeting | Test-Comp TOOLympics | ||
11:33 11mMeeting | SV-COMP TOOLympics | ||
11:45 11mMeeting | RERS TOOLympics | ||
11:56 11mMeeting | SAT TOOLympics | ||
12:07 11mMeeting | SL-COMP TOOLympics | ||
12:18 11mMeeting | TermCOMP TOOLympics | ||
11:00 - 12:30 | |||
11:00 30m | Invited Talk: Expected Cost Analysis of Attack-Defence Trees SPIoT Jan Kretinsky Technical University of Munich | ||
11:30 30mTalk | 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 30mTalk | The Refinement-Risk Loop - A Process for Security Engineering in Isabelle SPIoT Florian Kammüller Middlesex University, UK | ||
11:00 - 12:30 | |||
11:00 45mTalk | Computational Causal Discovery and its Applications CREST Sisi Ma University of Minnesota File Attached | ||
11:45 45mTalk | 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 | |||
11:00 30mTalk | 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 30mTalk | Automatic Synthesis of Polynomial Probabilistic Invariants via Geometric Persistence QAPL Pre-print | ||
12:00 30mTalk | Towards Digital Twins for the Description of Automotive Software Systems QAPL Jan Olaf Blech Aalto University Pre-print | ||
11:00 - 12:00 | |||
11:00 30mFull-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 30mFull-paper | Concurrent Typestate-Oriented Programming in Java PLACES | ||
11:00 - 12:30 | |||
11:00 30mTalk | 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 30mTalk | Rejection-Based Simulation of Stochastic Spreading Processes on Complex Networks HSB | ||
12:00 30mTalk | 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 | |||
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 60mTutorial | Hand-on Synthesis Experience with BoSy (part 2) SYNT Camp Leander Tentrup Saarland University | ||
13:30 - 15:30 | |||
13:30 45mTalk | Parametric Markov chains: algorithms, complexity and applications SynCoP Christel Baier TU Dresden, Germany | ||
14:15 45mTalk | Parametric Verification and Synthesis based on Gaussian Processes SynCoP | ||
13:30 - 15:30 | |||
14:00 45mTalk | 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 45mTalk | Type-Based Resource Analysis on Haskell DICE-FOPARA | ||
13:30 - 15:30 | |||
13:30 30mTalk | Full Abstraction for the Quantum Lambda-Calculus GaLoP | ||
14:00 30mTalk | Some ideas for a finite geometry of interaction model of second-order MLL GaLoP | ||
14:30 30mTalk | Bouncing Threads for Infinitary and Circular Proofs GaLoP | ||
15:00 30mTalk | Towards Circular Proof Nets GaLoP | ||
13:30 - 15:30 | |||
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 30mTalk | Coinduction in Uniform: what's next? HCVS Link to publication | ||
15:00 30mFull-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 | |||
13:30 60mTalk | Keynote: Shared Session Types for Safe, Practical Concurrency PLACES Stephanie Balzer Carnegie Mellon University | ||
14:30 30mFull-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 30mFull-paper | Service Equivalence via Multiparty Session Type Isomorphisms PLACES | ||
14:00 - 15:30 | |||
14:00 30mTalk | How to survive being a woman in computer science Mentoring Workshop Marieke Huisman University of Twente | ||
14:30 30mTalk | Advice on your adviser Mentoring Workshop Marsha Chechik University of Toronto File Attached | ||
15:00 30mTalk | A few lessons from the PhD I just finished Mentoring Workshop Juliana Franco Microsoft Research, Cambridge | ||
14:00 - 15:30 | |||
14:00 11mMeeting | CASC TOOLympics | ||
14:11 11mMeeting | CoCo TOOLympics | ||
14:22 11mMeeting | CRV TOOLympics | ||
14:33 11mMeeting | SMT-COMP TOOLympics | ||
14:45 11mMeeting | MCC TOOLympics | ||
14:56 11mMeeting | REC TOOLympics | ||
15:07 11mMeeting | Rodeo TOOLympics | ||
15:18 11mMeeting | VerifyThis TOOLympics | ||
14:00 - 15:30 | |||
14:00 30mTalk | 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 30mTalk | Learning from attacks and failures: generating reliability models from data SPIoT Marielle Stoelinga University of Twente and Radboud University, Nijmegen | ||
15:00 30mTalk | Graph-based Technique for Survivability Estimation and Optimization of IoT Applications SPIoT | ||
14:00 - 15:30 | |||
14:00 45mTalk | Coalgebras for causality CREST Matteo Sammartino University College London File Attached | ||
14:45 45mTalk | Causality and diagrammatic reasoning CREST Jean Krivine CNRS | ||
14:00 - 15:30 | |||
14:00 60mTalk | Invited talk: Exact and Approximate Reductions of Quantitative Models QAPL | ||
15:00 30mTalk | Coherent Resolutions of Nondeterminism QAPL Marco Bernardo University of Urbino | ||
14:00 - 15:30 | |||
14:00 60mTalk | 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 30mTalk | 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 | |||
16:00 45mTalk | Applications of Linear Defeasible Logic: combining resource consumption and exceptions to energy management and business processes DICE-FOPARA | ||
16:00 - 18:00 | |||
16:00 30mTalk | 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 30mExperience report | Report on the CHC competition HCVS Grigory Fedyukovich Princeton University | ||
16:00 - 18:00 | |||
16:00 2hMeeting | 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 | |||
16:00 45mTalk | Analysis, Repair and Causality for Timed Diagnostic Traces CREST Stefan Leue University of Konstanz File Attached | ||
16:45 25mResearch paper | Justification Based Reasoning in Dynamic Conflict Resolution [Werner Damm, Martin Franzle, Willem Hagemann, Paul Kroger, Astrid Rakow] CREST File Attached | ||
17:10 25mResearch paper | Towards A Logical Account of Epistemic Causality [Shakil M. Khan, Mikhail Soutchanski] CREST File Attached | ||
16:00 - 18:00 | |||
16:00 30mTalk | 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 30mTalk | An Adequate Semantics for Hybrid While QAPL | ||
17:00 30mTalk | Recent Applications and Quantitative Aspects of Spatial Model Checking QAPL | ||
17:30 30mTalk | Equational Characterization Metaresults for Bisimulation and Trace Semantics in ULTraS QAPL Marco Bernardo University of Urbino | ||
16:00 - 18:00 | |||
16:00 30mFull-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 30mTalk | 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 30mTalk | The Cpi-calculus: a Model for Confidential Name Passing PLACES Ivan Prokić University of Novi Sad | ||
17:30 5mDay closing | Closing remarks PLACES | ||
16:00 - 18:00 | |||
16:00 30mTalk | 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 30mTalk | 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 30mTalk | 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 10mDay closing | Closing HSB | ||
16:30 - 17:30 | |||
17:00 30mTalk | 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 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 8 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
07:30 - 08:30 | |||
08:40 - 09:00 | |||
08:40 20mSocial 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 | |||
09:00 60mTalk | Software Assurance in an Uncertain World Keynotes Marsha Chechik University of Toronto Link to publication File Attached | ||
10:30 - 12:30 | |||
10:30 30mTalk | Trees in Partial Higher Dimensional AutomataBest paper nomination FOSSACS Link to publication | ||
11:00 30mTalk | 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 30mTalk | Change Actions: Models of Generalised Differentiation FOSSACS Link to publication | ||
12:00 30mTalk | 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 | |||
10:30 30mTalk | 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 30mTalk | Parallel SAT Simplification on GPU Architectures TACAS Link to publication | ||
11:30 30mTalk | 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 30mTalk | 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 | ||
14:00 - 16:00 | Categories and (Co)algebraFOSSACS at MOON Chair(s): Sergey Goncharov FAU Erlangen-Nürnberg, Lehrstuhl 8 | ||
14:00 30mTalk | Equational Axiomatization of Algebras wth Structure FOSSACS Link to publication | ||
14:30 30mTalk | 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 30mTalk | 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 30mTalk | Coalgebra Learning via Duality FOSSACS Link to publication | ||
14:00 - 16:00 | |||
14:00 30mTalk | 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 30mTalk | 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 30mTalk | Computing Coupled Similarity TACAS Link to publication | ||
15:30 30mTalk | Reachability Analysis for Termination and Confluence of Rewriting TACAS Link to publication | ||
14:00 - 16:00 | |||
14:00 30mTalk | 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 30mTalk | 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 30mTalk | Counters in Kappa: Semantics, Simulation, and Static Analysis ESOP Link to publication | ||
15:30 30mTalk | One Step at a Time ESOP Link to publication | ||
16:30 - 18:00 | |||
16:30 90mTalk | An overview of Satisfiability Modulo Theories and its applications Tutorials Cesare Tinelli University of Iowa Link to publication | ||
16:30 - 18:00 | |||
16:30 30mTalk | Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks TACAS Link to publication | ||
17:00 30mTalk | 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 30mTalk | Extending a Brainiac Prover to Lambda-Free Higher-Order Logic TACAS Link to publication | ||
17:00 - 18:00 | |||
17:00 60mTalk | 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 | |||
Tue 9 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 9 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
08:00 - 09:00 | |||
09:00 - 10:00 | |||
09:00 60mTalk | On infinite duration games Keynotes Thomas Colcombet IRIF, University Paris Diderot and CNRS, France Link to publication File Attached | ||
10:30 - 12:30 | |||
10:30 30mTalk | 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 30mTalk | Automatic Modeling for Opaque Code in JavaScript Static Analysis FASE Link to publication | ||
11:30 30mTalk | 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 30mTalk | A Hybrid Dynamic Logic for Event/Data-based SystemsBest paper nomination FASE Link to publication | ||
10:30 - 12:30 | |||
10:30 30mTalk | Justness: A Completeness Criterion for Capturing Liveness Properties FOSSACS Link to publication | ||
11:00 30mTalk | 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 30mTalk | A Sound and Complete Logic for Algebraic Effects FOSSACS Link to publication | ||
12:00 30mTalk | Strong Adequacy and Untyped Full-Abstraction for Probabilistic Coherence Spaces FOSSACS Link to publication | ||
10:30 - 12:30 | |||
10:30 30mTalk | Handling polymorphic algebraic effects ESOP Link to publication | ||
11:00 30mTalk | 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 30mTalk | Types by Need ESOP Link to publication | ||
12:00 30mTalk | Verifiable certificates for predicate subtyping ESOP Link to publication | ||
14:00 - 15:00 | |||
14:00 30mTalk | 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 30mTalk | Verifiably Safe Off-Model Reinforcement Learning TACAS Link to publication | ||
14:00 - 16:00 | |||
14:00 30mTalk | A Dialectica-Like Interpretation of a Linear MSO on Infinite Words FOSSACS Link to publication | ||
14:30 30mTalk | Higher-order distributions for differential linear logic FOSSACS Link to publication | ||
15:00 30mTalk | Causality in Linear Logic: Full Completeness and Injectivity (unit-free multiplicative-additive fragment) FOSSACS Link to publication | ||
15:30 30mTalk | Resource-Tracking Concurrent Games FOSSACS Link to publication | ||
14:00 - 16:00 | |||
14:00 30mTalk | Extended call-by-push-value: reasoning about effectful programs and evaluation orderBest paper nomination ESOP Link to publication | ||
14:30 30mTalk | Effectful Normal-Form Bisimulation ESOP Link to publication | ||
15:00 30mTalk | On the Multi-Language Construction ESOP Link to publication | ||
15:30 30mTalk | Probabilistic Programming Inference via Intensional Semantics ESOP Link to publication | ||
16:30 - 18:00 | |||
16:30 90mDemonstration | Interactive session with tools and demos (I) TACAS | ||
16:30 - 18:00 | |||
16:30 30mTalk | VoxLogicA: a Spatial Model Checker for Declarative Image Analysis TACAS Link to publication | ||
17:00 30mTalk | On Reachability in Parameterized Phaser Programs TACAS Link to publication | ||
17:30 30mTalk | Abstract Dependency Graphs and Their Application to Model CheckingBest paper nomination TACAS Link to publication | ||
16:30 - 18:00 | |||
16:30 90mTalk | Software Verification — An Overview of the State of the Art Tutorials Dirk Beyer LMU Munich File Attached | ||
17:00 - 18:00 | |||
17:00 60mTalk | A tale of two MURIs: Authorization Meets Model Checking Mentoring Workshop Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc. | ||
18:00 - 20:00 | |||
18:00 2hMeeting | 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 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Wed 10 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
08:00 - 09:00 | |||
09:00 - 10:00 | |||
09:00 60mTalk | 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 30mTalk | Pyro: Generating Domain-Specific Collaborative Online Modeling Environments FASE Link to publication | ||
11:00 30mTalk | Efficient Model Synchronization by Automatically Constructed Repair ProcessesBest paper nomination FASE Link to publication | ||
11:30 30mTalk | Offline Delta-driven Model Transformation with Dependency Injection FASE Artur Boronat University of Leicester Link to publication | ||
12:00 30mTalk | A Logic-Based Incremental Approach to Graph Repair FASE Link to publication | ||
10:30 - 12:30 | |||
10:30 30mTalk | Optimal Satisfiability Checking for Arithmetic mu-Calculi FOSSACS Link to publication | ||
11:00 30mTalk | Two-Way Parikh Automata with a Visibly Pushdown Stack FOSSACS Link to publication | ||
11:30 30mTalk | Constructing Inductive-Inductive Types in Cubical Type Theory FOSSACS Link to publication | ||
12:00 30mTalk | Towards a Structural Proof Theory of Probabilistic mu–calculi FOSSACS Link to publication | ||
10:30 - 12:30 | |||
10:30 30mTalk | Multi-Core On-The-Fly Saturation TACAS Link to publication | ||
11:00 30mTalk | Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude TACAS Link to publication | ||
11:30 30mTalk | 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 30mTalk | 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 | |||
10:30 30mTalk | 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 30mTalk | 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 30mTalk | Safe Deferred Memory Reclamation with Types ESOP Link to publication | ||
12:00 30mTalk | 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 | |||
13:00 60mDemonstration | Interactive session with tools and demos (II) TACAS | ||
13:00 - 14:00 | |||
13:00 60mMeeting | ETAPS eV General Assembly Social | ||
14:00 - 16:00 | |||
14:00 30mTalk | DeepFault: Fault Localization For Deep Neural Networks FASE Link to publication | ||
14:30 30mTalk | 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 30mTalk | Formal Verification of Safety & Security Related Timing Constraints for A Cooperative Automotive System FASE Link to publication | ||
15:30 30mTalk | 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 | |||
14:00 30mTalk | 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 30mTalk | Continuous Reachability for Unordered Data Petri Nets is in PTime FOSSACS Link to publication | ||
15:00 30mTalk | Languages ordered by the subword order FOSSACS Link to publication | ||
15:30 30mTalk | Deciding Equivalence of Separated Non-Nested Attribute Systems in Polynomial Time FOSSACS Link to publication | ||
14:00 - 16:00 | |||
14:00 30mTalk | Tail Probabilities for Runtimes of Randomized Programs: Martingale Synthesis for Higher Moments TACAS Link to publication | ||
14:30 30mTalk | Computing the Expected Execution Time of Probabilistic Workflow Nets TACAS Link to publication | ||
15:00 30mTalk | 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 30mTalk | Optimal Time-Bounded Reachability Analysis for Concurrent Systems TACAS Link to publication | ||
14:00 - 16:00 | |||
14:00 30mTalk | 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 30mTalk | 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 30mTalk | A Categorical Model of an i/o-typed pi-calculus ESOP Link to publication | ||
15:30 30mTalk | A Process Algebra for Link Layer Protocols ESOP Link to publication | ||
16:30 - 18:00 | |||
16:30 30mTalk | iRank: a variable order metric for DEDS subject to linear invariants TACAS Link to publication | ||
17:00 30mTalk | Edge-Specified Reduction Binary Decision Diagrams TACAS Link to publication | ||
17:30 30mTalk | 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 | |||
17:00 60mTalk | Formal methods can be practical: Verifying time-critical systems Mentoring Workshop Reinhard Wilhelm Saarland University | ||
19:30 - 23:00 | |||
19:30 3h30mSocial Event | Banquet Social Jan Kofroň Charles University | ||
Thu 11 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Thu 11 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
09:00 - 10:00 | |||
09:00 60mTalk | Towards Efficient and Precise Concurrent Software Analysis Keynotes Cormac Flanagan University of California, Santa Cruz File Attached | ||
10:30 - 12:30 | |||
10:30 30mTalk | 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 30mTalk | A Formal Analysis of Timing Channel Security via Bucketing POST Link to publication | ||
11:30 30mTalk | 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 30mTalk | 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 | |||
10:30 30mTalk | Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware Approach TACAS Link to publication | ||
11:00 30mTalk | StocHy: automated verification and synthesis of stochastic processes TACAS Link to publication | ||
11:30 30mTalk | 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 30mTalk | Environmentally-friendly GR(1) Synthesis TACAS Link to publication | ||
10:30 - 12:30 | Program Analysis and Automated VerificationESOP at SUN II Chair(s): Stephanie Balzer Carnegie Mellon University | ||
10:30 30mTalk | Data-Races and Static Analysis for Interrupt-Driven Kernels ESOP Link to publication | ||
11:00 30mTalk | An abstract domain for trees with numeric relations ESOP Link to publication | ||
11:30 30mTalk | A static higher-order dependency pair framework ESOP Link to publication | ||
12:00 30mTalk | 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 30mTalk | CLTestCheck: Measuring Test Effectiveness for GPU Kernels FASE Link to publication | ||
14:30 30mTalk | 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 30mTalk | 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 30mTalk | A Data Flow Model with Frequency Arithmetic FASE Link to publication | ||
14:00 - 16:00 | |||
14:00 30mTalk | 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 30mTalk | Generalised Differential Privacy for Text Document Processing POST Link to publication | ||
15:00 30mTalk | Symbolic verification of distance bounding protocols POST Link to publication | ||
15:30 30mTalk | On the formalisation of Σ-Protocols and Commitment Schemes POST Link to publication | ||
14:00 - 16:00 | |||
14:00 30mTalk | Digital Bifurcation Analysis of TCP Dynamics TACAS Link to publication | ||
14:30 30mTalk | 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 30mTalk | 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 30mTalk | 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 | |||
14:00 30mTalk | Tight Worst-Case Bounds for Polynomial Loop Programs FOSSACS Link to publication | ||
14:30 30mTalk | Kleene algebra with hypotheses FOSSACS Link to publication | ||
15:00 30mTalk | The Impatient May Use Limited Optimism to Minimize Regret FOSSACS Link to publication | ||
15:30 30mTalk | Partial and Conditional Expectations in Markov Decision Processes with Integer Weights FOSSACS Link to publication | ||
16:30 - 18:00 | |||
16:30 30mTalk | CoVeriTest: Cooperative, Verifier-Based Testing FASE Link to publication | ||
17:00 30mTalk | Pardis: Priority Aware Test Case Reduction FASE Link to publication | ||
17:30 30mTalk | 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 | |||
16:30 30mTalk | 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 30mTalk | Verifying liquidity of Bitcoin contracts POST 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 30mTalk | Specification and Efficient Monitoring Beyond STL TACAS Link to publication | ||
17:00 30mTalk | 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 30mTalk | Constraint-based Monitoring of Hyperproperties TACAS Link to publication | ||
16:30 - 17:00 | |||
16:30 30mTalk | The Bernays-Schoenfinkel-Ramsey Class of Separation Logic on Arbitrary DomainsBest paper nomination FOSSACS Link to publication | ||