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

ETAPS 2014 Programme Tuesday April 8th

Tuesday, April 8th
09h00 - 10h00 Room: Amphitheater
FASE Invited Speaker (chair: Arend Rensink)
Christel Baier (Technical University of Dresden, Germany)
Probabilistic model checking and non-standard multi-objective reasoning
10h00 - 10h30 Coffee Break
10h30 - 12h30 ESOP / Room: Mont Blanc
Type Systems (chair: Matthias Felleisen)
  • Justin Slepak, Olin Shivers and Panagiotis Manolios. An Array-Oriented Language with Static Rank Polymorphism (nomination for best paper award)
  • Peter Thiemann and Luminous Fennell. Gradual Typing for Annotated Type Systems
  • Boris Düdder, Moritz Martens and Jakob Rehof. Staged Composition Synthesis
  • Jesper Cockx, Frank Piessens and Dominique Devriese. Overlapping and Order-Independent Patterns
FASE / Room: Kilimandjaro
Modelling and model transformation (chair: Reiko Heckel)
  • Alcino Cunha, Nuno Macedo and Tiago Guimarães. Target oriented relational model finding
  • Perdita Stevens. Bidirectionally tolerating inconsistency: partial transformations (nomination for best paper award)
  • Daniel Strueber, Julia Rubin, Gabriele Taentzer and Marsha Chechik. Splitting Models Using Information Retrieval and Model Crawling Techniques
  • Uli Fahrenberg, Mathieu Acher, Axel Legay and Andrzej Wasowski. Sound Merging and Differencing for Class Diagrams
FOSSACS / Room: Makalu
Probabilistic systems (chair: Holger Hermanns)
  • Nathalie Bertrand, Eric Fabre, Stefan Haar, Serge Haddad and Loic Helouet. Active diagnosis for probabilistic systems
  • Remi Bonnet, Stefan Kiefer and Anthony Widjaja Lin. Analysis of Probabilistic Basic Parallel Processes
  • Laurent Doyen, Thierry Massart and Mahsa Shirmohammadi. Limit Synchronization in Markov Decision Processes
  • Hongfei Fu. Maximal Cost-Bounded Reachability Probability on Continuous-Time Markov Decision Processes
TACAS / Room: Amphitheater
Modeling and model checking discrete systems (chair: Bernhard Steffen)
  • Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov and A.W. Roscoe. FDR3 - A Modern Refinement Checker for CSP
  • Gavin Lowe. Concurrent Depth-First Search Algorithms
  • Jan Reineke and Stavros Tripakis. Basic Problems in Multi-View Modeling
  • Anton Wijs and Dragan Bosnacki. GPUexplore: Many-Core On-the-Fly State Space Exploration Using GPUs
12h30 - 14h00 Lunch
14h00 - 15h00 Room: Amphitheater
POST Invited Speaker (chair: Martín Abadi)
David Mazières (Stanford University, US)
Security and the Average Programmer
15h00 - 16h00 ESOP / Room: Mont Blanc
Verified Compilation (chair: Steve Zdancewic)
  • Lennart Beringer, Gordon Stewart, Robert Dockins and Andrew W. Appel. Verified Compilation for Shared-Memory C
  • James T. Perconti and Amal Ahmed. Verifying an Open Compiler Using Multi-Language Semantics
FASE / Room: Kilimandjaro
Time and performance (chair: Christel Baier)
  • José Luiz Fiadeiro and Antonia Lopes. Heterogeneous and Asynchronous Networks of Timed Systems
  • Matthias Kowal, Ina Schaefer and Mirco Tribastone. Family-Based Performance Analysis of Variant-Rich Software Systems
FOSSACS / Room: Makalu
Semantics of programming languages (chair: Simona Ronchi della Rocca)
  • Luca Padovani. Type Reconstruction for the Linear pi-Calculus with Composite and Equi-Recursive Types (nomination for best paper award)
  • Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability
POST / Room: Cervin
Cryptography in Implementations (chair: Riccardo Focardi)
  • Ralf Kuesters, Enrico Scapin, Tomasz Truderung and Juergen Graf. Extending and Applying a Framework for the Cryptographic Verification of Java Programs
  • Manuel Barbosa, David Castro and Paulo Silva. Compiling CAO: from Cryptographic Specifications to C Implementations
16h00 - 16h30 Coffee Break
16h30 - 18h00 ESOP / Room: Mont Blanc
Program Verification I (chair: Xavier Leroy)
  • Kasper Svendsen and Lars Birkedal. Impredicative Concurrent Abstract Predicates
  • Philippa Gardner, Gian Ntzik and Adam Wright. Local Reasoning about File Systems
  • Véronique Benzaken, Evelyne Contejean and Stefania Dumbrava. A Coq Formalization of the Relational Data Model
  TUTORIAL / Room: Makalu (chair: Joost-Pieter Katoen)


Andrew D. Gordon (Microsoft Research and University of Edinburgh, UK)


Probabilistic Programming: what the Practical Programmer needs to know!

POST / Room: Cervin
Policies and Attacks (chair: Andrew Myers)
  • Gilles Barthe, Boris Köpf, Laurent Mauborgne and Martin Ochoa. Leakage Resilience against Concurrent Cache Attacks (nomination for best paper award)
  • Michael Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe and Cesar Sanchez. Temporal Logics for Hyperproperties
  • Petar Tsankov, Srdjan Marinovic, Mohammad Torabi Dashti and David Basin. Decentralized Composite Access Control