Program - ETAPS 2019

Tobias RungeTU Braunschweig, Ina SchaeferTechnische Universität Braunschweig, Loek CleophasEindhoven University of Technology (TU/e) and Stellenbosch University, Thomas ThümTU Braunschweig, Germany, Derrick KourieStellenbosch University, Bruce W Watson

11:00 - 11:30
Talk

Automatic Modeling for Opaque Code in JavaScript Static Analysis

Joonyoung Park, Alexander JordanOracle Labs, Australia, Sukyoung RyuKAIST, South Korea

11:30 - 12:00
Talk

SMT-Based Bounded Schedulability Analysis of the Clock Constraint Specification Language

Min ZhangEast China Normal University, Fu Song, Frederic MalletUniversité Côte d'Azur, France, Xiaohong Chen

12:00 - 12:30
Talk

A Hybrid Dynamic Logic for Event/Data-based Systems

Rolf HennickerLudwig Maximilians University Munich, Germany, Alexandre Madeira, Alexander Knapp

10:30 - 12:30: ESOP 2019 - Types at ESOP

10:30 - 11:00
Talk

Handling polymorphic algebraic effects

Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan

11:00 - 11:30
Talk

Distributive Disjoint Polymorphism for Compositional Programming

Xuan BiThe University of Hong Kong, Ningning XieThe University of Hong Kong, Bruno C. d. S. OliveiraThe University of Hong Kong, Hong Kong, Tom SchrijversKU Leuven

11:30 - 12:00
Talk

Types by Need

Beniamino AccattoliInria & Ecole Polytechnique, Giulio Guerrieri, Maico Leberle

12:00 - 12:30
Talk

Verifiable certificates for predicate subtyping

Frédéric Gilbert

14:00 - 16:00: ESOP 2019 - Program Semantics at ESOP

14:00 - 14:30
Talk

Extended call-by-push-value: reasoning about effectful programs and evaluation order

Dylan McDermottUniversity of Cambridge, Alan MycroftUniversity of Cambridge

14:30 - 15:00
Talk

Effectful Normal-Form Bisimulation

Ugo Dal LagoUniversity of Bologna / Inria, Francesco Gavazzo

15:00 - 15:30
Talk

On the Multi-Language Construction

Samuele BuroUniversità degli Studi di Verona, Isabella MastroeniUniversity of Verona, Italy

15:30 - 16:00
Talk

Probabilistic Programming Inference via Intensional Semantics

Simon CastellanImperial College London, UK, Hugo PaquetUniversity of Cambridge

14:00 - 16:00: FOSSACS 2019 - Resource Logics at FoSSaCS

14:00 - 14:30
Talk

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

Colin Riba, Pierre Pradic

14:30 - 15:00
Talk

Higher-order distributions for differential linear logic

Marie Kerjean, Jean-Simon Lemay

15:00 - 15:30
Talk

Causality in Linear Logic: Full Completeness and Injectivity (unit-free multiplicative-additive fragment)

Simon CastellanImperial College London, UK, Nobuko YoshidaImperial College London

15:30 - 16:00
Talk

Resource-Tracking Concurrent Games

Aurore Alcolei, Pierre ClairambaultCNRS & ENS Lyon, Olivier LaurentCNRS & ENS Lyon

14:00 - 15:00: TACAS 2019 - Synthesis at FASE

14:00 - 14:15
Talk

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:15 - 14:30
Talk

Environmentally-friendly GR(1) Synthesis

Rupak MajumdarMPI-SWS, Germany, Nir Piterman, Anne-Kathrin Schmuck

14:30 - 14:45
Talk

StocHy: automated verification and synthesis of stochastic processes

Nathalie CauchiUniversity of Oxford, Alessandro AbateUniversity of Oxford

14:45 - 15:00
Talk

Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware Approach

Mahmoud KhaledTU Munich, Eric Kim, Murat Arcak, Majid Zamani

14:00 - 16:00: TACAS 2019 - Tool Demos at TACAS

14:00 - 14:15
Talk

nonreach – A Tool for Nonreachability Analysis

Florian Messner, Christian SternagelUniversity of Innsbruck, Austria

14:15 - 14:30
Talk

The Quantitative Verification Benchmark Set

Arnd HartmannsUniversity of Twente, Michaela KlauckSaarland Informatics Campus, Saarland University, David ParkerUniversity of Birmingham, Tim Quatmann, Enno Ruijters

14:30 - 14:45
Talk

ILAng: A Modeling Platform for SoC Verification using Instruction-Level Abstractions

Bo-Yuan HuangPrinceton University, USA, Hongce Zhang, Aarti GuptaPrinceton University, Sharad MalikPrinceton University

14:45 - 15:00
Talk

MetAcsl: Specification and Verification of High-Level Properties

Virgile Robles, Nikolai KosmatovCEA List, Virgile PrevostoCEA Tech List, Pascale Le Gall

15:00 - 15:15
Talk

ROLL 1.0: $\omega$-Regular Language Learning Library

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

15:15 - 15:30
Talk

Symbolic Regex Matcher

Margus VeanesMicrosoft Research, Olli Saarikivi, Eric Xu, Tiki Wan

15:30 - 15:45
Talk

COMPASS 3.0

Marco Bozzano, Harold Bruintjes, Alessandro CimattiFondazione Bruno Kessler, Joost-Pieter KatoenRWTH Aachen University, Thomas NollRWTH Aachen University, Stefano TonettaFondazione Bruno Kessler, Italy

15:45 - 16:00
Talk

Debugging of Behavioural Models with CLEAR

Gianluca BarbonUniversit� Grenoble Alpes, Inria, LIG, Vincent LeroyUniversity of Grenoble - CNRS, Gwen SalaŸnUniversity of Grenoble Alpes

16:30 - 18:00: Tutorials - Beyer at ESOP

16:30 - 18:00
Talk

Software Verification — An Overview of the State of the Art

Dirk BeyerLMU Munich

16:30 - 18:00: TACAS 2019 - Machine Learning at TACAS

16:30 - 17:15
Talk

Omega-Regular Objectives in Model-Free Reinforcement Learning

Ernst Moritz HahnQueen's University Belfast, Mateo Perez, Sven ScheweUniversity of Liverpool, Fabio Somenzi, Ashutosh Trivedi, Dominik Wojtczak

17:15 - 18:00
Talk

Verifiably Safe Off-Model Reinforcement Learning

Nathan FultonMIT-IBM Watson AI Lab, André PlatzerCarnegie Mellon University

17:00 - 18:00: Mentoring Workshop - Reps at FASE

17:00 - 18:00
Talk

A tale of two MURIs: Authorization Meets Model Checking

Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.

Wed 10 Apr

09:00 - 10:00: Keynotes - Fisher at ESOP

09:00 - 10:00
Talk

From quadcopters to helicopters: Formal verification to eliminate exploitable bugs

Kathleen FisherTufts University

10:30 - 12:30: FOSSACS 2019 - Fixed-point Logics at FoSSaCS

10:30 - 11:00
Talk

Optimal Satisfiability Checking for Arithmetic mu-Calculi

Daniel Hausmann, Lutz SchöderFAU Erlangen-Nürnberg, Lehrstuhl 8

11:00 - 11:30
Talk

Identifiers in Registers – Describing Network Algorithms with Logic

Benedikt BolligCNRS, LSV, ENS Paris-Saclay, Patricia BouyerLSV, CNRS & ENS Cachan, University Paris Saclay, Fabian Reiter

11:30 - 12:00
Talk

Towards a Structural Proof Theory of Probabilistic mu–calculi

Matteo Mio, Christophe Lucas

12:00 - 12:30
Talk

Constructing Inductive-Inductive Types in Cubical Type Theory

Jasper Hugunin

10:30 - 12:30: TACAS 2019 - Model Checking at TACAS

10:30 - 11:10
Talk

VoxLogicA: a Spatial Model Checker for Declarative Image Analysis

Gina Belmonte, Vincenzo Ciancia, Diego Latella, Mieke MassinkCNR-ISTI Pisa, Italy

11:10 - 11:50
Talk

On Reachability in Parameterized Phaser Programs

Petru Eles, Zeinab Ganjei, Ludovic HenrioCNRS, Zebo Peng, Ahmed Rezine

11:50 - 12:30
Talk

Abstract Dependency Graphs and Their Application to Model Checking

Søren Enevoldsen, Kim LarsenAalborg University, Jiri Srba

10:30 - 12:30: FASE 2019 - Model-driven Development and Model Transformation at FASE

10:30 - 11:00
Talk

Pyro: Generating Domain-Specific Collaborative Online Modeling Environments

Philip Zweihoff, Stefan Naujokat, Bernhard SteffenTechnical University Dortmund

11:00 - 11:30
Talk

Efficient Model Synchronization by Automatically Constructed Repair Processes

Lars Fritsche, Jens Kosiol, Andy SchürrTU Darmstadt, Gabriele TaentzerUniversität Marburg

11:30 - 12:00
Talk

Offline Delta-driven Model Transformation with Dependency Injection

Artur BoronatUniversity of Leicester

12:00 - 12:30
Talk

A Logic-Based Incremental Approach to Graph Repair

Sven Schneider, Leen Lambers, Fernando OrejasUniversitat Politècnica de Catalunya, Spain

10:30 - 12:30: ESOP 2019 - Security and Incremental Computation at ESOP

10:30 - 11:00
Talk

Robustly Safe Compilation

Marco PatrignaniSaarland University & CISPA, Deepak GargMax Planck Institute for Software Systems

11:00 - 11:30
Talk

Compiling Sandboxes: Formally Verified Software Fault Isolation

Frédéric Besson, Sandrine BlazyUniv Rennes- IRISA, Alexandre Dang, Thomas P. JensenINRIA Rennes, Pierre WilkeYale University

11:30 - 12:00
Talk

Fixing Incremental Computation: Derivatives of fixpoints, and the recursive semantics of Datalog

Michael Peyton JonesIOHK, Mario Alvarez-PicalloUniversity of Oxford, Alexander Eyers-TaylorSemmle, Luke OngUniversity of Oxford

12:00 - 12:30
Talk

Incremental λ-Calculus in Cache-Transfer Style, Static Memoization by Program Transformation

Paolo G. GiarrussoEPFL, Switzerland, Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2, Philipp SchusterUniversity of Tübingen, Germany

12:30 - 14:00: Social - General Assembly at ESOP

12:30 - 14:00
Meeting

ETAPS eV General Assembly

14:00 - 16:00: FOSSACS 2019 - Automata at FoSSaCS

14:00 - 14:30
Talk

Two-Way Parikh Automata with a Visibly Pushdown Stack

Luc Dartois, Emmanuel Filiot, Jean-Marc Talbot

14:30 - 15:00
Talk

Deciding Equivalence of Separated Non-Nested Attribute Systems in Polynomial Time

Helmut SeidlTechnische Universität München, Raphaela Palenta, Sebastian Maneth

15:00 - 15:30
Talk

Continuous Reachability for Unordered Data Petri Nets is in PTime

Utkarsh Gupta, Preey Shah, S. Akshay, Piotr Hofman

15:30 - 16:00
Talk

Languages ordered by the subword order

Dietrich Kuske, Georg ZetzscheMax Planck Institute for Software Systems (MPI-SWS)

14:00 - 16:00: ESOP 2019 - Concurrency and Distribution at ESOP

14:00 - 14:30
Talk

Asynchronous timed session types: duality and time-sensitive processes

Laura BocchiUniversity of Kent, Maurizio Murgia, Vasco Thudichum Vasconcelos, Nobuko YoshidaImperial College London

14:30 - 15:00
Talk

Manifest Deadlock-Freedom for Shared Session Types

Stephanie BalzerCarnegie Mellon University, Bernardo ToninhoNOVA-LINCS, FCT/UNL, Frank PfenningCarnegie Mellon University, USA

15:00 - 15:30
Talk

A Categorical Model of an i/o-typed pi-calculus

Ken Sakayori, Takeshi TsukadaUniversity of Tokyo, Japan

15:30 - 16:00
Talk

A Process Algebra for Link Layer Protocols

Rob van Glabbeek, Peter Höfner, Michael Markl

14:00 - 16:00: TACAS 2019 - Concurrent and Distributed Systems at TACAS

14:00 - 14:30
Talk

Checking Deadlock-Freedom of Parametric Component-Based Systems

Marius BozgaVerimag/CNRS, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Joseph SifakisVerimag/CNRS

14:30 - 15:00
Talk

The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Expressivity and Usability

Olav Bunte, Jan Friso Groote, Jeroen J.A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton WijsEindhoven University of Technology, Tim A.C. Willemse

15:00 - 15:30
Talk

Automatic Analysis of Consistency Properties of Distributed Transaction Systems in Maude

Si Liu, Peter Ölveczky, Min ZhangEast China Normal University, Qi Wang, José Meseguer

15:30 - 16:00
Talk

Multi-Core On-The-Fly Saturation

Tom van Dijk, Jeroen Meijer, Jaco van de PolAarhus University

14:00 - 16:00: FASE 2019 - Software Verification II at FASE

14:00 - 14:30
Talk

DeepFault: Fault Localization For Deep Neural Networks

Hasan Ferit Eniser, Simos Gerasimou, Alper Sen

14:30 - 15:00
Talk

Variability Abstraction and Refinement for Game-based Lifted Model Checking of full CTL

Aleksandar S. DimovskiIT University of Copenhagen, Denmark, Axel LegayINRIA Rennes, Andrzej WąsowskiIT University of Copenhagen, Denmark

15:00 - 15:30
Talk

Formal Verification of Safety & Security Related Timing Constraints for A Cooperative Automotive System

Huang Li, Eun-Young KangUniversity of Southern Denmark

15:30 - 16:00
Talk

Checking Observational Purity Of Procedures

Himanshu Arora, Raghavan KomondoorIndian Institute of Science, Bangalore, G. RamalingamMicrosoft Research

16:30 - 18:00: TACAS 2019 - Symbolic Verification at TACAS

16:30 - 17:00
Talk

iRank: a variable order metric for DEDS subject to linear invariants

Elvio Gilberto Amparore, Gianfranco Ciardo, Susanna Donatelli, Andrew Miner

17:00 - 17:30
Talk

Edge-Specified Reduction Binary Decision Diagrams

Junaid Babar, Chuan Jiang, Gianfranco Ciardo, Andrew Miner

17:30 - 18:00
Talk

Effective Entailment Checking for Separation Logic with Inductive Definitions

Jens Katelaan, Christoph MathejaRWTH Aachen University, Florian ZulegerVienna University of Technology

17:00 - 18:00: Mentoring Workshop - Wilhelm at FASE

17:00 - 18:00
Talk

Formal methods can be practical: Verifying time-critical systems

Reinhard WilhelmSaarland University

Thu 11 Apr

09:00 - 10:00: Keynotes - Flanagan at TACAS

09:00 - 10:00
Talk

Towards Efficient and Precise Concurrent Software Analysis

Cormac FlanaganUniversity of California, Santa Cruz

10:30 - 12:30: POST 2019 - Covert Channels and Information Flow at POST

10:30 - 11:00
Talk

Towards parallel information flow control foundations

Marco VassenaChalmers University of Technology, Gary Soeller, Peter Amidon, Matthew Chan, John RennerUniversity of California, San Diego, Deian StefanUniversity of California San Diego

11:00 - 11:30
Talk

A Formal Analysis of Timing Channel Security via Bucketing

Tachio TerauchiWaseda University, Timos AntonopoulosYale University

11:30 - 12:00
Talk

A Dependently Typed Library for Static Information-Flow Control in Idris

Søren Eller ThomsenAarhus University, Aslan AskarovAarhus University, Simon GregersenAarhus University

12:00 - 12:30
Talk

Achieving Safety Incrementally with Checked C

Andrew Ruef, Ian Sweet, Leonidas LampropoulosUniversity of Pennsylvania, Michael HicksUniversity of Maryland, College Park, David Tarditi

10:30 - 12:30: TACAS 2019 - Hybrid and Stochastic Systems at TACAS

10:30 - 11:00
Talk

Tail Probabilities for Runtimes of Randomized Programs: Martingale Synthesis for Higher Moments

Satoshi Kura, Natsuki Urabe, Ichiro HasuoNational Institute of Informatics

11:00 - 11:30
Talk

Computing the Expected Execution Time of Probabilistic Workflow Nets

Philipp J. Meyer, Javier Esparza, Philip Offtermatt

11:30 - 12:00
Talk

Shepherding Hordes of Markov Chains

Milan CeskaBrno University of Technology , Nils JansenRWTH Aachen University, Sebastian JungesRWTH Aachen University, Germany, Joost-Pieter KatoenRWTH Aachen University

12:00 - 12:30
Talk

Optimal Time-Bounded Reachability Analysis for Concurrent Systems

Yuliya Butkova, Gereon Fox

10:30 - 12:30: ESOP 2019 - Program Analysis and Automated Verification at FoSSaCS

10:30 - 11:00
Talk

Data-Races and Static Analysis for Interrupt-Driven Kernels

Nikita Chopra, R Rekha, Deepak D'Souza

11:00 - 11:30
Talk

An abstract domain for trees with numeric relations

Matthieu Journault, Antoine MinéUPMC, France, Abdelraouf Ouadjaout

11:30 - 12:00
Talk

A static higher-order dependency pair framework

Carsten Fuhs, Cynthia Kop

12:00 - 12:30
Talk

Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses

Henning Basold, Ekaterina KomendantskayaHeriot-Watt University, UK, Yue LiHeriot-Watt University, UK

10:30 - 12:30: FASE 2019 - Software Evolution & Requirements Engineering at FASE

10:30 - 11:00
Talk

Structural and Nominal Cross-Language Clone Detection

Lawton Nichols, Mehmet EmreUniversity of California, Santa Barbara, Ben HardekopfUC Santa Barbara

11:00 - 11:30
Talk

SL2SF: Refactoring Simulink to Stateflow

Stephen Wynn-Williams, Zinovy Diskin, Vera Pantelic, Mark LawfordMcMaster, Gehan Selim, Curtis Milo

11:30 - 12:00
Talk

Metric Temporal Graph Logic over Typed Attributed Graphs

Holger GieseHasso Plattner Institute, University of Potsdam, Maria Maximova, Lucas Sakizloglou, Sven Schneider

12:00 - 12:15
Talk

KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Programs

Qian Jiaqi, Min ZhangEast China Normal University, Yi WangShenzhen University, Kazuhiro Ogata

12:15 - 12:30
Talk

Business Process Privacy Analysis in PLEAK

Aivo Toots, Reedik Tuuling, Maksym Yerokhin, Marlon Dumas, Luciano García-BañuelosUniversity of Tartu, Peeter Laud, Raimundas Matulevicius, Alisa Pankova, Martin Pettai, Pille Pullonen, Jake Tom

14:00 - 16:00: POST 2019 - Privacy and Protocols at POST

14:00 - 14:30
Talk

Wys*: A Verified Language Extension for Secure Multi-party Computations

Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research, Michael HicksUniversity of Maryland, College Park

14:30 - 15:00
Talk

Generalised Differential Privacy for Text Document Processing

Natasha Fernandes, Mark Dras, Annabelle McIverMacquarie University

15:00 - 15:30
Talk

Symbolic verification of distance bounding protocols

Alexandre Debant, Stephanie Delaune

15:30 - 16:00
Talk

On the formalisation of Σ-Protocols and Commitment Schemes

David Butler, David Aspinall, Adria Gascon

14:00 - 16:00: TACAS 2019 - Safety and Fault-tolerant Systems at TACAS

14:00 - 14:30
Talk

Digital Bifurcation Analysis of TCP Dynamics

Nikola Benes, Lubos Brim, Samuel Pastva, David SafranekMasaryk University

14:30 - 15:00
Talk

Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Model Checking

Ilina StoilkovskaVienna University of Technology , Igor KonnovInria Nancy, Josef WidderTU Wien, Florian ZulegerVienna University of Technology

15:00 - 15:30
Talk

Measuring Masking Fault-Tolerance

Pablo CastroDept. of Computer Science FCEFQyN, University of Rio Cuarto, Pedro D'Argenio, Ramiro Demasi, Luciano Putruele

15:30 - 16:00
Talk

PhASAR: An Inter-Procedural Static Analysis Framework for C/C++

Philipp Dominik SchubertHeinz Nixdorf Institut, Paderborn University, Ben HermannUniversity of Paderborn, Eric BoddenHeinz Nixdorf Institut, Paderborn University and Fraunhofer IEM

14:00 - 16:00: FASE 2019 - Specification, Design, and Implementation of Particular Classes of Systems at FASE

14:00 - 14:30
Talk

CLTestCheck: Measuring Test Effectiveness for GPU Kernels

Chao PengUniversity of Edinburgh, UK, Ajitha RajanUniversity of Edinburgh

14:30 - 15:00
Talk

Implementing SOS with Active Objects: A Case Study of a Multicore Memory System

Nikolaos Bezirgiannis, Frank S. de BoerCentrum Wiskunde & Informatica, Leiden University, Einar Broch JohnsenUniversity of Oslo, Ka I Pun, Silvia Lizeth Tapia TarifaUniversity of Oslo

15:00 - 15:30
Talk

Optimal and Automated Deployment for Microservices

Mario BravettiUniversità di Bologna, Saverio GiallorenzoUniversity of Southern Denmark, Jacopo MauroUniversity of Southern Denmark, Iacopo Talevi, Gianluigi Zavattaro

15:30 - 16:00
Talk

A Data Flow Model with Frequency Arithmetic

Paul Dubrulle, Stéphane Louise, Christophe Gaston, Nikolai KosmatovCEA List, Arnault Lapitre

14:00 - 16:00: FOSSACS 2019 - Verification at FoSSaCS

14:00 - 14:30
Talk

Tight Worst-Case Bounds for Polynomial Loop Programs

Amir Ben-Amram, Geoff Hamilton

14:30 - 15:00
Talk

Kleene algebra with hypotheses

Amina Doumane, Denis Kuperberg, Damien PousCNRS, Pierre Pradic

15:00 - 15:30
Talk

The Impatient May Use Limited Optimism to Minimize Regret

Michaël Cadilhac, Guillermo A. PerezUniversity of Antwerp, Marie van den Bogaard

15:30 - 16:00
Talk

Partial and Conditional Expectations in Markov Decision Processes with Integer Weights

Jakob Piribauer, Christel BaierTU Dresden, Germany

16:30 - 17:30: POST 2019 - Distributed Systems at POST

16:30 - 17:00
Talk

Orchestrating Layered Attestations

John D. Ramsdell, Paul D. Rowe, Perry Alexander, Sarah Helble, J. Aaron Pendergrass, Adam Petz, Peter Loscocco

17:00 - 17:30
Talk

Verifying liquidity of Bitcoin contracts

Massimo Bartoletti, Roberto Zunino

16:30 - 18:00: TACAS 2019 - Monitoring and Runtime Verification at TACAS

16:30 - 17:00
Talk

Specification and Efficient Monitoring Beyond STL

Alexey Bakhirkin, Nicolas Basset

17:00 - 17:30
Talk

VyPR2: A Framework for Runtime Verification of Python Web Services

Joshua DawesUniversity of Manchester and CERN, Giles RegerUniversity of Manchester, Giovanni Franzoni, Andreas Pfeiffer, Giacomo Govi

17:30 - 18:00
Talk

Constraint-based Monitoring of Hyperproperties

Christopher Hahn, Marvin Stenger, Leander TentrupSaarland University

16:30 - 18:00: FASE 2019 - Software Testing at FASE

16:30 - 17:00
Talk

CoVeriTest: Cooperative, Verifier-Based Testing

Dirk BeyerLMU Munich, Marie-Christine JakobsLMU, Munich, Germany

17:00 - 17:30
Talk

Pardis: Priority Aware Test Case Reduction

Golnaz Gharachorlu, Nick SumnerSimon Fraser University

17:30 - 18:00
Talk

Automatically Identifying Sufficient Object Builders from Module APIs

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

16:30 - 17:00: FOSSACS 2019 - Verification (continued) at FoSSaCS

16:30 - 17:00
Talk

The Bernays-Schoenfinkel-Ramsey Class of Separation Logic on Arbitrary Domains

Mnacho Echenim, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Nicolas Peltier

Sat 6 Apr 2019


Room	9:00	30	10:00	30	11:00	30	12:00	30	13:00	30	14:00		30	15:00	30	16:00	30	17:00	30	18:00	30	19:00	30
BEHAPI	BEHAPI I 09:00 - 10:30				BEHAPI II 11:00 - 12:30						BEHAPI III 14:00 - 15:30					BEHAPI IV 16:00 - 18:00
DICE-FOPARA	DICE-FOPARA I 09:00 - 10:30				DICE-FOPARA II 11:00 - 12:30						DICE-FOPARA III 14:00 - 15:30					DICE-FOPARA IV 16:00 - 18:00
GaLoP	GaLoP I 09:00 - 10:30				GaLoP II 11:00 - 12:30						GaLoP III 14:00 - 15:30					GaLoP IV 16:00 - 18:00
HSB	HSB I 09:00 - 10:30				HSB II 11:00 - 12:30						HSB III 14:00 - 15:30					HSB IV 16:00 - 18:00
InterAVT	InterAVT I 09:00 - 10:30				InterAVT II 11:00 - 12:30						InterAVT III 14:00 - 15:30					InterAVT IV 16:00 - 18:00
LiVe	LiVe I 09:00 - 10:30				LiVe II 11:00 - 12:30						LiVe III 14:00 - 15:30					LiVe IV 16:00 - 18:00
MeTRiD	MeTRiD I 09:00 - 10:30				MeTRiD II 11:00 - 12:30						MeTRiD III 14:00 - 15:30					MeTRiD IV 16:00 - 18:00
Mentoring												ETAPS Mentoring Workshop 17:30 - 19:00
PERR	PERR I 09:00 - 10:30				PERR II 11:00 - 12:30						PERR III 14:00 - 15:30					PERR IV 16:00 - 18:00
QAPL	QAPL I 09:00 - 10:30				QAPL II 11:00 - 12:30						QAPL III 14:00 - 15:30					QAPL IV 16:00 - 18:00
SynCoP	SynCoP 09:00 - 10:30				SynCoP 11:00 - 12:30						SynCoP 14:00 - 15:30					SynCoP 16:00 - 18:00
TOOLympics-Large	ETAPS TOOLympics CoCo 09:00 - 10:30				ETAPS TOOLympics SL-COMP 11:00 - 12:30						ETAPS TOOLympics RERS 1 14:00 - 15:30					ETAPS TOOLympics RERS 2 16:00 - 18:00
TOOLympics-SmallA	ETAPS TOOLympics SV-COMP Talks 09:00 - 10:30				ETAPS TOOLympics SV-COMP Meeting 11:00 - 12:30						ETAPS TOOLympics Test-Comp Talks 14:00 - 15:30					ETAPS TOOLympics Test-Comp Meeting 16:00 - 18:00
TOOLympics-SmallB	ETAPS TOOLympics VerifyThis 1 09:00 - 10:30				ETAPS TOOLympics VerifyThis 2 11:00 - 12:30						ETAPS TOOLympics VerifyThis 3 14:00 - 15:30					ETAPS TOOLympics VerifyThis 4 16:00 - 18:00
VerifyThis	VerifyThis 09:00 - 10:30				VerifyThis 11:00 - 12:30						VerifyThis 14:00 - 15:30					VerifyThis 16:00 - 18:00

Sun 7 Apr 2019


Room	9:00	30	10:00	30	11:00	30	12:00	30	13:00	30	14:00	30	15:00	30	16:00	30	17:00	30	18:00	30
CREST	CREST I 09:00 - 10:30				CREST II 11:00 - 12:30						CREST III 14:00 - 15:30				CREST IV 16:00 - 18:00
DICE-FOPARA	DICE-FOPARA V 09:00 - 10:30				DICE-FOPARA VI 11:00 - 12:30						DICE-FOPARA VII 14:00 - 15:30				DICE-FOPARA VIII 16:00 - 18:00
GaLoP	GaLoP V 09:00 - 10:30				GaLoP VI 11:00 - 12:30						GaLoP VII 14:00 - 15:30				GaLoP VIII 16:00 - 18:00
HCVS	HCVS I 09:00 - 10:30				HCVS II 11:00 - 12:30						HCVS III 14:00 - 15:30				HCVS IV 16:00 - 18:00
HSB	HSB V 09:00 - 10:30				HSB VI 11:00 - 12:30						HSB VII 14:00 - 15:30				HSB VIII 16:00 - 18:00
Mentoring	ETAPS Mentoring Workshop 09:00 - 09:30	ETAPS Mentoring Workshop Morning Session I 09:30 - 10:30				ETAPS Mentoring Workshop Morning Session II 11:30 - 12:30					ETAPS Mentoring Workshop Afternoon Session I 14:00 - 15:30					ETAPS Mentoring Workshop Afternoon Session II 16:30 - 17:30
PLACES	PLACES I 09:00 - 10:30				PLACES II 11:00 - 12:30						PLACES III 14:00 - 15:30				PLACES IV 16:00 - 18:00
QAPL	QAPL 09:00 - 10:30				QAPL 11:00 - 12:30						QAPL 14:00 - 15:30				QAPL 16:00 - 18:00
SPIoT	SPIoT 09:00 - 10:30				SPIoT 11:00 - 12:30						SPIoT 14:00 - 15:30				SPIoT 16:00 - 18:00
SYNT camp	SYNT Camp 09:00 - 10:30				SYNT Camp 11:00 - 12:30						SYNT Camp 14:00 - 15:30				SYNT Camp 16:00 - 18:00
SynCoP	SynCoP 09:00 - 10:30				SynCoP 11:00 - 12:30						SynCoP 14:00 - 15:30				SynCoP 16:00 - 18:00
TOOLympics-Large	ETAPS TOOLympics 09:00 - 10:30				ETAPS TOOLympics TOOLympics 1 - Pre-Events 11:00 - 12:30						ETAPS TOOLympics TOOLympics 2 - On-Site / Post 14:00 - 15:30				ETAPS TOOLympics 25 Years TACAS 16:00 - 18:00
TOOLympics-SmallB	ETAPS TOOLympics VerifyThis 5 09:00 - 10:30				ETAPS TOOLympics VerifyThis 6 11:00 - 12:30
VerifyThis	VerifyThis 09:00 - 10:30				VerifyThis 11:00 - 12:30						VerifyThis 14:00 - 15:30				VerifyThis 16:00 - 18:00

Mon 8 Apr 2019


Room	9:00	30	10:00	30	11:00	30	12:00	30	13:00	30	14:00	30	15:00	30	16:00	30	17:00	30	18:00	30
ESOP	ETAPS Keynotes Chechik 09:00 - 10:00			ESOP Program Verification 10:30 - 12:30							ESOP Language Design 14:00 - 16:00						ETAPS Mentoring Workshop Vitek 17:00 - 18:00
FoSSaCS				FOSSACS Applied Categories 10:30 - 12:30							FOSSACS Categories and (Co)algebra 14:00 - 16:00					ETAPS Tutorials Tinelli 16:30 - 18:00
TACAS				TACAS SAT and SMT I 10:30 - 12:30							TACAS Verification and Analysis 14:00 - 16:00					TACAS SAT Solving and Theorem Proving 16:30 - 18:00

Tue 9 Apr 2019


Room	9:00	30	10:00	30	11:00	30	12:00	30	13:00	30	14:00	30	15:00	30	16:00	30	17:00	30	18:00	30
ESOP				ESOP Types 10:30 - 12:30							ESOP Program Semantics 14:00 - 16:00					ETAPS Tutorials Beyer 16:30 - 18:00
FASE				FASE Software Verification I 10:30 - 12:30							TACAS Synthesis 14:00 - 15:00						ETAPS Mentoring Workshop Reps 17:00 - 18:00
FoSSaCS	ETAPS Keynotes Colcombet 09:00 - 10:00			FOSSACS Semantics 10:30 - 12:30							FOSSACS Resource Logics 14:00 - 16:00
TACAS				TACAS SAT and SMT II 10:30 - 12:30							TACAS Tool Demos 14:00 - 16:00					TACAS Machine Learning 16:30 - 18:00

Wed 10 Apr 2019


Room	9:00	30	10:00	30	11:00	30	12:00	30	13:00	30	14:00	30	15:00	30	16:00	30	17:00	30	18:00	30
ESOP	ETAPS Keynotes Fisher 09:00 - 10:00			ESOP Security and Incremental Computation 10:30 - 12:30				ETAPS Social General Assembly 12:30 - 14:00			ESOP Concurrency and Distribution 14:00 - 16:00
FASE				FASE Model-driven Development and Model Transformation 10:30 - 12:30							FASE Software Verification II 14:00 - 16:00						ETAPS Mentoring Workshop Wilhelm 17:00 - 18:00
FoSSaCS				FOSSACS Fixed-point Logics 10:30 - 12:30							FOSSACS Automata 14:00 - 16:00
TACAS				TACAS Model Checking 10:30 - 12:30							TACAS Concurrent and Distributed Systems 14:00 - 16:00					TACAS Symbolic Verification 16:30 - 18:00

Thu 11 Apr 2019


Room	9:00	30	10:00	30	11:00	30	12:00	30	13:00	30	14:00	30	15:00	30	16:00	30	17:00	30	18:00	30
FASE				FASE Software Evolution & Requirements Engineering 10:30 - 12:30							FASE Specification, Design, and Implementation of Particular Classes of Systems 14:00 - 16:00					FASE Software Testing 16:30 - 18:00
FoSSaCS				ESOP Program Analysis and Automated Verification 10:30 - 12:30							FOSSACS Verification 14:00 - 16:00					FOSSACS Verification (continued) 16:30 - 17:00	ETAPS Mentoring Workshop 17:00 - 18:00
POST				POST Covert Channels and Information Flow 10:30 - 12:30							POST Privacy and Protocols 14:00 - 16:00					POST Distributed Systems 16:30 - 17:30
TACAS	ETAPS Keynotes Flanagan 09:00 - 10:00			TACAS Hybrid and Stochastic Systems 10:30 - 12:30							TACAS Safety and Fault-tolerant Systems 14:00 - 16:00					TACAS Monitoring and Runtime Verification 16:30 - 18:00

Sun 7 Apr 2019


Room	9:00	15	30	45	10:00	15	30	45	11:00		15		30		45		12:00		15		30	45	13:00	15	30	45	14:00		15		30		45		15:00		15		30	45	16:00	15	30	45	17:00	15	30	45
Mentoring			ETAPS Mentoring WorkshopKeynote From Shape Analysis to Smart Contract Verification: A journey in proof ... 09:30 - 10:30										ETAPS Mentoring Workshop How to Give an Effective Talk 11:30 - 12:00				ETAPS Mentoring Workshop Navigating through the academic jungle: tips, tricks & traps 12:00 - 12:30										ETAPS Mentoring Workshop How to survive being a woman in computer science 14:00 - 14:30				ETAPS Mentoring Workshop Advice on your adviser 14:30 - 15:00				ETAPS Mentoring Workshop A few lessons from the PhD I just finished 15:00 - 15:30								ETAPS Mentoring Workshop Gentle introduction to language design research: Why get involved, open ... 16:30 - 17:00		ETAPS Mentoring Workshop Science and Sanity: how to do the former while retaining the later (Panel) 17:00 - 17:30
TOOLympics-Large									ETAPS TOOLympics SL-COMP 11:00 - 11:11	ETAPS TOOLympics CHC-COMP 11:11 - 11:22		ETAPS TOOLympics QComp 11:22 - 11:33		ETAPS TOOLympics RERS 11:33 - 11:45	ETAPS TOOLympics SAT 11:45 - 11:56	ETAPS TOOLympics SV-COMP 11:56 - 12:07		ETAPS TOOLympics TermCOMP 12:07 - 12:18		ETAPS TOOLympics Test-Comp 12:18 - 12:30							ETAPS TOOLympics CASC 14:00 - 14:11	ETAPS TOOLympics CRV 14:11 - 14:22		ETAPS TOOLympics CoCo 14:22 - 14:33		ETAPS TOOLympics MCC 14:33 - 14:45	ETAPS TOOLympics REC 14:45 - 14:56	ETAPS TOOLympics Rodeo 14:56 - 15:07		ETAPS TOOLympics SMT-COMP 15:07 - 15:18		ETAPS TOOLympics VerifyThis 15:18 - 15:30

Mon 8 Apr 2019


Room	9:00	15	30	45	10:00	15	30	45	11:00	15	30	45	12:00	15	30	45	13:00	15	30	45	14:00	15	30	45	15:00	15	30	45	16:00	15	30	45	17:00	15	30	45	18:00	15	30	45
ESOP	ETAPS Keynotes Software Assurance in an Uncertain World 09:00 - 10:00						ESOP Time Credits and Time Receipts in Iris 10:30 - 11:00		ESOP Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms 11:00 - 11:30		ESOP Semi-Automated Reasoning About Non-Determinism in C Expressions 11:30 - 12:00		ESOP Safe Deferred Memory Reclamation with Types 12:00 - 12:30								ESOP Codata in Action 14:00 - 14:30		ESOP Composing bidirectional programs monadically 14:30 - 15:00		ESOP Counters in Kappa: Semantics, Simulation, and Static Analysis 15:00 - 15:30		ESOP One Step at a Time 15:30 - 16:00						ETAPS Mentoring Workshop Do programming languages matter for correctness of code? A reproduction ... 17:00 - 18:00
FoSSaCS							FOSSACS Trees in Partial Higher Dimensional Automata 10:30 - 11:00		FOSSACS Rewriting Abstract Structures: Materialization Explained Categorically 11:00 - 11:30		FOSSACS Change Actions: Models of Generalised Differentiation 11:30 - 12:00		FOSSACS Causal Inference by String Diagram Surgery 12:00 - 12:30								FOSSACS Equational Axiomatization of Algebras wth Structure 14:00 - 14:30		FOSSACS Equational Theories and Monads from Polynomial Cayley Representations 14:30 - 15:00		FOSSACS Path category for free - Open morphisms from coalgebras with non-determ ... 15:00 - 15:30		FOSSACS Coalgebra Learning via Duality 15:30 - 16:00				ETAPS Tutorials An overview of Satisfiability Modulo Theories and its applications 16:30 - 18:00
TACAS							TACAS Decomposing Farkas Interpolants 10:30 - 11:00		TACAS Parallel SAT Simplification on GPU Architectures 11:00 - 11:30		TACAS Encoding Redundancy for Satisfaction-Driven Clause Learning 11:30 - 12:00		TACAS WAPS: Weighted and Projected Sampling 12:00 - 12:30								TACAS LCV: A Verification Tool for Linear Controller Software 14:00 - 14:30		TACAS Semantic Fault Localization and Suspiciousness Ranking 14:30 - 15:00		TACAS Computing Coupled Similarity 15:00 - 15:30		TACAS Reachability Analysis for Termination and Confluence of Rewriting 15:30 - 16:00				TACAS Quantitative Verification of Masked Arithmetic Programs against Side-Ch ... 16:30 - 17:00		TACAS Incremental Analysis of Evolving Alloy Models 17:00 - 17:30		TACAS Extending a Brainiac Prover to Lambda-Free Higher-Order Logic 17:30 - 18:00

Tue 9 Apr 2019


Room	9:00	15	30	45	10:00	15	30	45	11:00	15	30	45	12:00	15	30	45	13:00	15	30	45	14:00	15	30	45	15:00	15	30	45	16:00	15	30	45	17:00	15	30	45	18:00	15	30	45
ESOP							ESOP Handling polymorphic algebraic effects 10:30 - 11:00		ESOP Distributive Disjoint Polymorphism for Compositional Programming 11:00 - 11:30		ESOP Types by Need 11:30 - 12:00		ESOP Verifiable certificates for predicate subtyping 12:00 - 12:30								ESOP Extended call-by-push-value: reasoning about effectful programs and eva ... 14:00 - 14:30		ESOP Effectful Normal-Form Bisimulation 14:30 - 15:00		ESOP On the Multi-Language Construction 15:00 - 15:30		ESOP Probabilistic Programming Inference via Intensional Semantics 15:30 - 16:00				ETAPS Tutorials Software Verification — An Overview of the State of the Art 16:30 - 18:00
FASE							FASE Tool Support for Correctness-by-Construction 10:30 - 11:00		FASE Automatic Modeling for Opaque Code in JavaScript Static Analysis 11:00 - 11:30		FASE SMT-Based Bounded Schedulability Analysis of the Clock Constraint Speci ... 11:30 - 12:00		FASE A Hybrid Dynamic Logic for Event/Data-based Systems 12:00 - 12:30								TACAS Minimal-Time Synthesis for Parametric Timed Automata 14:00 - 14:15	TACAS Environmentally-friendly GR(1) Synthesis 14:15 - 14:30	TACAS StocHy: automated verification and synthesis of stochastic processes 14:30 - 14:45	TACAS Synthesis of Symbolic Controllers: A Parallelized and Sparsity-Aware Ap ... 14:45 - 15:00									ETAPS Mentoring Workshop A tale of two MURIs: Authorization Meets Model Checking 17:00 - 18:00
FoSSaCS	ETAPS Keynotes On infinite duration games 09:00 - 10:00						FOSSACS Justness: A Completeness Criterion for Capturing Liveness Properties 10:30 - 11:00		FOSSACS A Complete Normal-Form Bisimilarity for State 11:00 - 11:30		FOSSACS A Sound and Complete Logic for Algebraic Effects 11:30 - 12:00		FOSSACS Strong Adequacy and Untyped Full-Abstraction for Probabilistic Coherenc ... 12:00 - 12:30								FOSSACS A Dialectica-Like Interpretation of a Linear MSO on Infinite Words 14:00 - 14:30		FOSSACS Higher-order distributions for differential linear logic 14:30 - 15:00		FOSSACS Causality in Linear Logic: Full Completeness and Injectivity (unit-free ... 15:00 - 15:30		FOSSACS Resource-Tracking Concurrent Games 15:30 - 16:00
TACAS							TACAS Building Better Bit-Blasting for Floating-Point Problems 10:30 - 11:00		TACAS The Axiom Profiler: Understanding and Debugging SMT Quantifier Instanti ... 11:00 - 11:30		TACAS On the Empirical Time Complexity of Scale-Free 3-SAT at the Phase Trans ... 11:30 - 12:00		TACAS Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painl ... 12:00 - 12:30								TACAS nonreach – A Tool for Nonreachability Analysis 14:00 - 14:15	TACAS The Quantitative Verification Benchmark Set 14:15 - 14:30	TACAS ILAng: A Modeling Platform for SoC Verification using Instruction-Level ... 14:30 - 14:45	TACAS MetAcsl: Specification and Verification of High-Level Properties 14:45 - 15:00	TACAS ROLL 1.0: $\omega$-Regular Language Learning Library 15:00 - 15:15	TACAS Symbolic Regex Matcher 15:15 - 15:30	TACAS COMPASS 3.0 15:30 - 15:45	TACAS Debugging of Behavioural Models with CLEAR 15:45 - 16:00			TACAS Omega-Regular Objectives in Model-Free Reinforcement Learning 16:30 - 17:15			TACAS Verifiably Safe Off-Model Reinforcement Learning 17:15 - 18:00

Wed 10 Apr 2019


Room	9:00	15	30	45	10:00	15	30	45	11:00		15	30	45		12:00	15	30	45	13:00	15	30	45	14:00	15	30	45	15:00	15	30	45	16:00	15	30	45	17:00	15	30	45	18:00	15	30	45
ESOP	ETAPS Keynotes From quadcopters to helicopters: Formal verification to eliminate explo ... 09:00 - 10:00						ESOP Robustly Safe Compilation 10:30 - 11:00		ESOP Compiling Sandboxes: Formally Verified Software Fault Isolation 11:00 - 11:30			ESOP Fixing Incremental Computation: Derivatives of fixpoints, and the recur ... 11:30 - 12:00			ESOP Incremental λ-Calculus in Cache-Transfer Style, Static Memoization by P ... 12:00 - 12:30		ETAPS Social ETAPS eV General Assembly 12:30 - 14:00						ESOP Asynchronous timed session types: duality and time-sensitive processes 14:00 - 14:30		ESOP Manifest Deadlock-Freedom for Shared Session Types 14:30 - 15:00		ESOP A Categorical Model of an i/o-typed pi-calculus 15:00 - 15:30		ESOP A Process Algebra for Link Layer Protocols 15:30 - 16:00
FASE							FASE Pyro: Generating Domain-Specific Collaborative Online Modeling Environments 10:30 - 11:00		FASE Efficient Model Synchronization by Automatically Constructed Repair Pro ... 11:00 - 11:30			FASE Offline Delta-driven Model Transformation with Dependency Injection 11:30 - 12:00			FASE A Logic-Based Incremental Approach to Graph Repair 12:00 - 12:30								FASE DeepFault: Fault Localization For Deep Neural Networks 14:00 - 14:30		FASE Variability Abstraction and Refinement for Game-based Lifted Model Chec ... 14:30 - 15:00		FASE Formal Verification of Safety & Security Related Timing Constraints for ... 15:00 - 15:30		FASE Checking Observational Purity Of Procedures 15:30 - 16:00						ETAPS Mentoring Workshop Formal methods can be practical: Verifying time-critical systems 17:00 - 18:00
FoSSaCS							FOSSACS Optimal Satisfiability Checking for Arithmetic mu-Calculi 10:30 - 11:00		FOSSACS Identifiers in Registers – Describing Network Algorithms with Logic 11:00 - 11:30			FOSSACS Towards a Structural Proof Theory of Probabilistic mu–calculi 11:30 - 12:00			FOSSACS Constructing Inductive-Inductive Types in Cubical Type Theory 12:00 - 12:30								FOSSACS Two-Way Parikh Automata with a Visibly Pushdown Stack 14:00 - 14:30		FOSSACS Deciding Equivalence of Separated Non-Nested Attribute Systems in Polyn ... 14:30 - 15:00		FOSSACS Continuous Reachability for Unordered Data Petri Nets is in PTime 15:00 - 15:30		FOSSACS Languages ordered by the subword order 15:30 - 16:00
TACAS							TACAS VoxLogicA: a Spatial Model Checker for Declarative Image Analysis 10:30 - 11:10			TACAS On Reachability in Parameterized Phaser Programs 11:10 - 11:50				TACAS Abstract Dependency Graphs and Their Application to Model Checking 11:50 - 12:30									TACAS Checking Deadlock-Freedom of Parametric Component-Based Systems 14:00 - 14:30		TACAS The mCRL2 Toolset for Analysing Concurrent Systems: Improvements in Exp ... 14:30 - 15:00		TACAS Automatic Analysis of Consistency Properties of Distributed Transaction ... 15:00 - 15:30		TACAS Multi-Core On-The-Fly Saturation 15:30 - 16:00				TACAS iRank: a variable order metric for DEDS subject to linear invariants 16:30 - 17:00		TACAS Edge-Specified Reduction Binary Decision Diagrams 17:00 - 17:30		TACAS Effective Entailment Checking for Separation Logic with Inductive Defin ... 17:30 - 18:00

Thu 11 Apr 2019


Room	9:00	15	30	45	10:00	15	30	45	11:00	15	30	45	12:00	15	30	45	13:00	15	30	45	14:00	15	30	45	15:00	15	30	45	16:00	15	30	45	17:00	15	30	45	18:00	15	30	45
FASE							FASE Structural and Nominal Cross-Language Clone Detection 10:30 - 11:00		FASE SL2SF: Refactoring Simulink to Stateflow 11:00 - 11:30		FASE Metric Temporal Graph Logic over Typed Attributed Graphs 11:30 - 12:00		FASE KupC: A Formal Tool for Modeling and Verifying Dynamic Updating of C Pr ... 12:00 - 12:15	FASE Business Process Privacy Analysis in PLEAK 12:15 - 12:30							FASE CLTestCheck: Measuring Test Effectiveness for GPU Kernels 14:00 - 14:30		FASE Implementing SOS with Active Objects: A Case Study of a Multicore Memor ... 14:30 - 15:00		FASE Optimal and Automated Deployment for Microservices 15:00 - 15:30		FASE A Data Flow Model with Frequency Arithmetic 15:30 - 16:00				FASE CoVeriTest: Cooperative, Verifier-Based Testing 16:30 - 17:00		FASE Pardis: Priority Aware Test Case Reduction 17:00 - 17:30		FASE Automatically Identifying Sufficient Object Builders from Module APIs 17:30 - 18:00
FoSSaCS							ESOP Data-Races and Static Analysis for Interrupt-Driven Kernels 10:30 - 11:00		ESOP An abstract domain for trees with numeric relations 11:00 - 11:30		ESOP A static higher-order dependency pair framework 11:30 - 12:00		ESOP Coinduction in Uniform: Foundations for Corecursive Proof Search with H ... 12:00 - 12:30								FOSSACS Tight Worst-Case Bounds for Polynomial Loop Programs 14:00 - 14:30		FOSSACS Kleene algebra with hypotheses 14:30 - 15:00		FOSSACS The Impatient May Use Limited Optimism to Minimize Regret 15:00 - 15:30		FOSSACS Partial and Conditional Expectations in Markov Decision Processes with ... 15:30 - 16:00				FOSSACS The Bernays-Schoenfinkel-Ramsey Class of Separation Logic on Arbitrary ... 16:30 - 17:00
POST							POST Towards parallel information flow control foundations 10:30 - 11:00		POST A Formal Analysis of Timing Channel Security via Bucketing 11:00 - 11:30		POST A Dependently Typed Library for Static Information-Flow Control in Idris 11:30 - 12:00		POST Achieving Safety Incrementally with Checked C 12:00 - 12:30								POST Wys*: A Verified Language Extension for Secure Multi-party Computations 14:00 - 14:30		POST Generalised Differential Privacy for Text Document Processing 14:30 - 15:00		POST Symbolic verification of distance bounding protocols 15:00 - 15:30		POST On the formalisation of Σ-Protocols and Commitment Schemes 15:30 - 16:00				POST Orchestrating Layered Attestations 16:30 - 17:00		POST Verifying liquidity of Bitcoin contracts 17:00 - 17:30
TACAS	ETAPS Keynotes Towards Efficient and Precise Concurrent Software Analysis 09:00 - 10:00						TACAS Tail Probabilities for Runtimes of Randomized Programs: Martingale Synt ... 10:30 - 11:00		TACAS Computing the Expected Execution Time of Probabilistic Workflow Nets 11:00 - 11:30		TACAS Shepherding Hordes of Markov Chains 11:30 - 12:00		TACAS Optimal Time-Bounded Reachability Analysis for Concurrent Systems 12:00 - 12:30								TACAS Digital Bifurcation Analysis of TCP Dynamics 14:00 - 14:30		TACAS Verifying Safety of Synchronous Fault-Tolerant Algorithms by Bounded Mo ... 14:30 - 15:00		TACAS Measuring Masking Fault-Tolerance 15:00 - 15:30		TACAS PhASAR: An Inter-Procedural Static Analysis Framework for C/C++ 15:30 - 16:00				TACAS Specification and Efficient Monitoring Beyond STL 16:30 - 17:00		TACAS VyPR2: A Framework for Runtime Verification of Python Web Services 17:00 - 17:30		TACAS Constraint-based Monitoring of Hyperproperties 17:30 - 18:00

iCalendar subscription service for your personal schedule

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

Currently Viewed Program

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

ETAPS 2019 Program

Sat 6 Apr

Sun 7 Apr

Mon 8 Apr

Tue 9 Apr

Wed 10 Apr

Thu 11 Apr

Sat 6 Apr 2019

BEHAPI

BEHAPI

BEHAPI

BEHAPI

DICE-FOPARA

DICE-FOPARA

DICE-FOPARA

DICE-FOPARA

GaLoP

GaLoP

GaLoP

GaLoP

HSB

HSB

HSB

HSB

InterAVT

InterAVT

InterAVT

InterAVT

LiVe

LiVe

LiVe

LiVe

MeTRiD

MeTRiD

MeTRiD

MeTRiD

ETAPS Mentoring Workshop

PERR

PERR

PERR

PERR

QAPL

QAPL

QAPL

QAPL

SynCoP

SynCoP

SynCoP

SynCoP

ETAPS TOOLympics

ETAPS TOOLympics

ETAPS TOOLympics

ETAPS TOOLympics

ETAPS TOOLympics

ETAPS TOOLympics

ETAPS TOOLympics

ETAPS TOOLympics

ETAPS TOOLympics

ETAPS TOOLympics

ETAPS TOOLympics

ETAPS TOOLympics

VerifyThis

VerifyThis

VerifyThis

VerifyThis

Sun 7 Apr 2019

CREST

CREST

CREST

CREST

DICE-FOPARA

DICE-FOPARA

DICE-FOPARA

DICE-FOPARA

GaLoP

GaLoP

GaLoP

GaLoP

HCVS

HCVS