| Wednesday, April 9th |
| 09h00 - 10h00 |
Room: Amphitheater
ETAPS Invited Speaker
Geoffrey Smith (Florida International University, US)
Operational Significance and Robustness in Quantitative Information Flow |
| 10h00 - 10h30 |
Coffee Break |
| 10h30 - 12h30 |
ESOP / Room: Mont Blanc
Semantics (chair: Dan Ghica)
- Raphaelle Crubille and Ugo Dal Lago. On Probabilistic Applicative Bisimulation and Call-by-Value Lambda Calculi
- Joaquin Aguado, Michael Mendler, Reinhard von Hanxleden and Insa Fuhrmann. Grounding Synchronous Deterministic Concurrency in Sequential Programming
- Paul Downen and Zena Ariola. The Duality of Construction
- Casper Bach Poulsen and Peter D. Mosses. Deriving Pretty-Big-Step Semantics from Small-Step Semantics
|
FASE / Room: Kilimandjaro
Static analysis (chair: Perdita Stevens)
- Pietro Ferrara, Daniel Schweizer and Lucas Brutschy. TouchCost: Cost Analysis of TouchDevelop Scripts
- Rashmi Mudduluru and Murali Krishna Ramanathan. Efficient Incremental Static Analysis Using Path Abstraction
- Wei Huang, Yao Dong and Ana Milanova. Type-based Taint Analysis of Java Web Applications
- Alireza Sadeghi, Naeem Esfahani and Sam Malek. Mining the Categorized Software Repositories to Improve the Analysis of Security Vulnerabilities
|
|
TACAS / Room: Amphitheater
Timed and hybrid systems I (chair: Christel Baier)
- Dieky Adzkiya, Bart De Schutter and Alessandro Abate. Forward Reachability Computation for Autonomous Max-Plus-Linear Systems
- Lacramioara Astefanoaei, Souha Ben Rayana, Saddek Bensalem, Marius Bozga and Jacques Combaz. Compositional Invariant Generation for Timed Systems
- Khalil Ghorbal and André Platzer. Characterizing Algebraic Invariants by Differential Radical Invariants
|
| 12h30 - 14h00 |
Lunch |
TACAS / Room: Atrium
Tool Demonstrations |
| 14h00 - 15h00 |
Room: Amphitheater
ESOP Invited Speaker (chair: Zhong Shao)
Maurice Herlihy (Brown University, US)
Why Concurrent Data Structures are Still Hard |
| 15h00 - 16h00 |
ESOP / Room: Mont Blanc
Concurrency (chair: Paul-Andre Mellies)
- Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey and Germán Andrés Delbianco. Communicating State Transition Systems for Fine-Grained Concurrent Resources
- Oren Zomer, Guy Golan-Gueta, G. Ramalingam and Mooly Sagiv. Checking Linearizability of Encapsulated Extended Operations
|
FASE / Room: Kilimandjaro
Scenario-based specification (chair: Ina Schaefer)
- Dimitri Van Landuyt and Wouter Joosen. Modularizing Early Architectural Assumptions in Scenario-based Requirements
- Barak Cohen and Shahar Maoz. Semantically Configurable Analysis of Scenario-Based Specifications
|
FOSSACS / Room: Makalu
Networks (chair: Anca Muscholl)
- Guy Avni, Orna Kupferman and Tami Tamir. Network-Formation Games with Regular Objectives
- Nathalie Bertrand, Paulin Fournier and Arnaud Sangnier. Playing with probabilities in Reconfigurable Broadcast Networks
|
TACAS / Room: Amphitheater
Timed and hybrid systems II (chair: Kim G. Larsen)
- Christian Herrera, Bernd Westphal and Andreas Podelski. Quasi-equal Clock Reduction: More Networks, More Queries
- Ting Wang, Jun Sun, Yang Liu, Xinyu Wang and Shanping Li. Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata
|
| 16h00 - 16h30 |
Coffee Break |
| 16h30 - 18h00 |
ESOP / Room: Mont Blanc
Linear Types (chair: Tarmo Uustalu)
- Dan Ghica and Alex I. Smith. Bounded Linear Types with Generalised Resources
- Aloïs Brunel, Marco Gaboardi, Damiano Mazza and Steve Zdancewic. A Core Quantitative Coeffect Calculus
- Akira Yoshimizu, Ichiro Hasuo, Claudia Faggian and Ugo Dal Lago. Measurements in Proof Nets as Higher-Order Quantum Circuits
|
FASE / Room: Kilimandjaro
Software verification (chair: Antonia Lopes)
- Paolo Masci, Yi Zhang, Paul Jones, Paul Curzon and Harold Thimbleby. Software verification for medical device user interfaces in PVS
- Pedro Gomes, Attilio Picoco and Dilian Gurov. Sound Control Flow Graph Extraction from Incomplete Java Bytecode Programs
- Marina Zaharieva-Stojanovski and Marieke Huisman. Verifying Class Invariants in Concurrent Programs
|
FOSSACS / Room: Makalu
Program analysis (chair: Paul-André Melliès)
- Naoki Kobayashi, Kazuhiro Inaba and Takeshi Tsukada. Unsafe Order-2 Tree Languages are Context-Sensitive (nomination for best paper award)
- Andrzej Murawski and Nikos Tzevelekos. Game semantics for nominal exceptions
- Takeshi Tsukada and Naoki Kobayashi. Complexity of Model-Checking Call-by-Value Programs
|
TACAS / Room: Amphitheater
Monitoring, fault detection and identification (chair: Klaus Havelund)
- Marco Bozzano, Alessandro Cimatti, Marco Gario and Stefano Tonetta. Formal design of Fault Detection and Identification components with Temporal Epistemic Logic (nomination for best paper award)
- Normann Decker, Martin Leucker and Daniel Thoma. Monitoring Modulo Theories
- Thomas Reinbacher, Kristin Yvonne Rozier and Johann Schumann. Temporal-Logic Based Runtime Observer Pairs for System Health Mangement of Real-Time Systems
|
| 20h00 - 23h00 |
Dinner at Château de Sassenage |