ETAPS 2017: 22-29 April 2017, Uppsala, Sweden

ETAPS 2017 Monday

Monday, April 24, 2017

Registration (Business)
08:00 – 08:30, Street Level

Plenary
08:30 – 09:00, Stora Salen, 6th Floor
Opening
Joost-Pieter Katoen and Parosh Aziz Abdulla
(RWTH Aachen University, Germany; Uppsala University, Sweden)

Plenary
09:00 – 10:00, Stora Salen, 6th Floor
Invited Talk: Validation, Synthesis and Optimization for Cyber-Physical Systems
Kim Guldstrand Larsen
(Aalborg University, Denmark)
Publisher's Version

Coffee Break
10:00 – 10:30, 3rd and 6th Floor

Coherence Spaces and Higher-Order Computation (FOSSACS)
10:30 – 12:30, Sal B
Session chair: Andrzej Murawski

Information Flow (POST)
10:30 – 12:30, Sal C
Session chair: Alejandro Russo
Verification Techniques 1 (TACAS)
10:30 – 12:30, Stora Salen, 6th Floor
Session chair: Axel Legay
Moved to Wednesday!

Coherence Spaces and Uniform Continuity

Kei Matsumoto
(Kyoto University, Japan)
Publisher's Version
Timing-Sensitive Noninterference through Composition
Willard Rafnsson, Limin Jia, and Lujo Bauer
(MPI-SWS, Germany; Carnegie Mellon University, USA)
Publisher's Version Preprint Info
An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP
(CNRS, France; IRISA, France; Inria, France)
Publisher's Version Preprint Info
The Free Exponential Modality of Probabilistic Coherence Spaces
Raphaëlle Crubillé, Thomas Ehrhard, Michele Pagani, and Christine Tasson
(University of Paris Diderot, France)
Publisher's Version
Quantifying Vulnerability of Secret Generation Using Hyper-Distributions
Mário S. Alvim, Piotr Mardziel, and Michael W. Hicks
(Federal University of Minas Gerais, Brazil; Carnegie Mellon University, USA; University of Maryland at College Park, USA)
Publisher's Version Preprint Info
Combining String Abstract Domains for JavaScript Analysis: An Evaluation
Roberto Amadini, Alexander Jordan, Graeme Gange, François Gauthier, Peter Schachte, Harald Søndergaard, Peter J. Stuckey, and Chenyi Zhang
(University of Melbourne, Australia; Oracle Labs, Australia; Oracle, Australia; University of Queensland, Australia)
Publisher's Version Preprint
From Qualitative to Quantitative Semantics - By Change of Base
James Laird
(University of Bath, UK)
Publisher's Version
A Principled Approach to Tracking Information Flow in the Presence of Libraries
Daniel Hedin, Alexander Sjösten, Frank Piessens, and Andrei Sabelfeld
(Mälardalen University, Sweden; Chalmers University of Technology, Sweden; KU Leuven, Belgium)
Publisher's Version Preprint
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani
(Fondazione Bruno Kessler, Italy; University of Trento, Italy)
Publisher's Version Preprint Info
Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence
Ryoma Sin'Ya, Kazuyuki Asada, Naoki Kobayashi, and Takeshi Tsukada
(University of Tokyo, Japan)
Publisher's Version
Secure Multi-party Computation: Information Flow of Outputs and Game Theory
Patrick Ah-Fat and Michael Huth
(Imperial College London, UK)
Publisher's Version
Bounded Quantifier Instantiation for Checking Inductive Invariants
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; University of Massachusetts at Amherst, USA)
Publisher's Version Preprint

Lunch
12:30 – 14:00, Sal D, Street Level

Algebra and Coalgebra (FOSSACS)
14:00 – 16:00, Sal B
Session chair: James Laird
Security Protocols (POST)
14:00 – 16:00, Sal C
Session chair: Mark Ryan
Verification Techniques 2 (TACAS)
14:00 – 16:00, Stora Salen, 6th Floor
Session chair: Kim Larsen
Algebra, Coalgebra, and Minimization in Polynomial Differential Equations
Michele Boreale
(University of Florence, Italy)
Best-Paper Award Nominee
Publisher's Version Preprint Info
Automated Verification of Dynamic Root of Trust Protocols
Sergiu Bursuc, Christian Johansen, and Shiwei Xu
(University of Bristol, UK; University of Oslo, Norway; Wuhan Digital and Engineering Institute, China)
Publisher's Version Preprint
Proving Termination Through Conditional Termination
Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, and Albert Rubio
(Universitat de Vic, Spain; Microsoft Research, UK; Universitat Politècnica de Catalunya, Spain)
Publisher's Version Preprint Info
Equational Theories of Abnormal Termination Based on Kleene Algebra
Konstantinos Mamouras
(University of Pennsylvania, USA)
Publisher's Version
Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols
(LORIA, France; CNRS, France; Inria, France; University of Lorraine, France; ETH Zurich, Switzerland)
Publisher's Version Preprint Info
Efficient Certified Resolution Proof Checking
(University of Southern Denmark, Denmark; University of Lisbon, Portugal)
Publisher's Version Preprint
Companions, Codensity and Causality
Damien Pous and Jurriaan Rot
(CNRS, France; ENS Lyon, France; Radboud University Nijmegen, Netherlands)
Publisher's Version Preprint
On Communication Models When Verifying Equivalence Properties
Kushal Babel, Vincent Cheval, and Steve Kremer
(IIT Bombay, India; Inria, France; LORIA, France; CNRS, France; University of Lorraine, France)
Best-Paper Award Nominee
Publisher's Version Preprint Info
Precise Widening Operators for Proving Termination by Abstract Interpretation
Nathanaël Courant and Caterina Urban
(ENS, France; ETH Zurich, Switzerland)
Publisher's Version Preprint
Nominal Automata with Name Binding
Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann
(University of Erlangen-Nuremberg, Germany; Cornell University, USA)
Publisher's Version Preprint
A Survey of Attacks on Ethereum Smart Contracts (SoK)
Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli
(University of Cagliari, Italy)
Publisher's Version Preprint
Automatic Verification of Finite Precision Implementations of Linear Controllers
Junkil Park, Miroslav Pajic, Oleg Sokolsky, and Insup Lee
(University of Pennsylvania, USA; Duke University, USA)
Publisher's Version Preprint

Coffee Break
16:00 – 16:30, 3rd and 6th Floor

Plenary
16:30 – 18:00, Stora Salen, 6th Floor
Learning (TACAS)
16:30 – 18:00, Sal B
Session chair: Bernhard Steffen
Tutorial: Secure composition of security protocols
Veronique Cortier
(CNRS, France)
Learning Symbolic Automata
(University of Wisconsin-Madison, USA)
Best-Paper Award Nominee
Publisher's Version Preprint
 
ML for ML: Learning Cost Semantics by Experiment
Ankush Das and Jan Hoffmann
(Carnegie Mellon University, USA)
Publisher's Version Preprint Info
 
A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees
Yong Li, Yu-Fang Chen, Lijun Zhang, and Depeng Liu
(Institute of Software at Chinese Academy of Sciences, China; Academia Sinica, Taiwan)
Publisher's Version Preprint

Reception
18:30 – 22:00, 6th Floor