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
(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
(Aalborg University, Denmark)
 Publisher's Version |
|||
| Coffee Break 10:00 – 10:30, 3rd and 6th Floor |
|||
|
Coherence Spaces and Higher-Order Computation (FOSSACS) |
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! |
Timing-Sensitive Noninterference through Composition
(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
(University of Paris Diderot, France)
Publisher's Version  |
Quantifying Vulnerability of Secret Generation Using Hyper-Distributions
(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
(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
(University of Bath, UK)
Publisher's Version |
A Principled Approach to Tracking Information Flow in the Presence of Libraries
(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
(Fondazione Bruno Kessler, Italy; University of Trento, Italy)
Publisher's Version Preprint Info |
|
|
Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence
(University of Tokyo, Japan)
Publisher's Version |
Secure Multi-party Computation: Information Flow of Outputs and Game Theory
(Imperial College London, UK)
Publisher's Version |
Bounded Quantifier Instantiation for Checking Inductive Invariants
(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
(University of Florence, Italy)
Best-Paper Award Nominee Publisher's Version Preprint Info |
Automated Verification of Dynamic Root of Trust Protocols
(University of Bristol, UK; University of Oslo, Norway; Wuhan Digital and Engineering Institute, China)
Publisher's Version Preprint  |
Proving Termination Through Conditional Termination
(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
(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
(CNRS, France; ENS Lyon, France; Radboud University Nijmegen, Netherlands)
Publisher's Version Preprint |
On Communication Models When Verifying Equivalence Properties
(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
(ENS, France; ETH Zurich, Switzerland)
Publisher's Version Preprint  |
|
|
Nominal Automata with Name Binding
(University of Erlangen-Nuremberg, Germany; Cornell University, USA)
Publisher's Version Preprint   |
A Survey of Attacks on Ethereum Smart Contracts (SoK)
(University of Cagliari, Italy)
Publisher's Version Preprint  |
Automatic Verification of Finite Precision Implementations of Linear Controllers
(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
(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
(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
(Institute of Software at Chinese Academy of Sciences, China; Academia Sinica, Taiwan)
Publisher's Version Preprint |
|||
| Reception 18:30 – 22:00, 6th Floor |
|||