ETAPS 2014: 5-13 April 2014, Grenoble, France

ETAPS 2014 Programme Wednesday April 9th

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