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

ETAPS 2014 Programme Monday April 7th

Monday, April 7th
08h30 - 09h00
Room: Amphitheater
ETAPS Opening
09h00 - 10h00 Room: Amphitheater
CC Invited Speaker (chair: Albert Cohen)
Benoit Dupont de Dinechin (Kalray, France)
Using the SSA-Form in a Code Generator
10h00 - 10h30 Coffee Break
10h30 - 12h30 CC / Room: Mont Blanc
Program Analysis and Optimization (chair: Paul Feautrier)
  • Andre Tavares, Benoit Boissinot, Fernando Pereira and Fabrice Rastello. Parameterized Construction of Program Representations for Sparse Dataflow Analyses (25mn)
  • Rishi Surendran, Rajkishore Barik, Jisheng Zhao and Vivek Sarkar. Inter-iteration Scalar Replacement Using Array SSA Form (25mn)
  • Venkatesh Srinivasan and Thomas Reps. Recovery of Class Hierarchies and Composition Relationships from Machine Code (25mn)
  • Amitabha Sanyal, Alan Mycroft, Amey Karkare and Rahul Asati. Liveness-Based Garbage Collection (25mn)
  • Henri-Pierre Charles, Damien Couroussé, Victor Lomüller, Fernando A. Endo and Rémy Gauguey. deGoal a tool to embed dynamic code generators into applications (Tool presentation, 15mn)
POST / Room: Makalu
Analysis of Cryptographic Protocols (chair: Steve Kremer)
  • David Baelde, Stéphanie Delaune and Lucca Hirschi. A Reduced Semantics for Deciding Trace Equivalence using Constraint Systems
  • Myrto Arapinis, Jia Liu, Eike Ritter and Mark Ryan. Stateful Applied Pi Calculus
  • Michael Backes, Esfandiar Mohammadi and Tim Ruffing. Computational Soundness Results for ProVerif: Bridging the Gap from Trace Properties to Uniformity
  • David Lubicz, Graham Steel and Marion Daubignard. A Secure Key Management Interface with Asymmetric Cryptography
TACAS / Room: Amphitheater
Decision procedures and their application in analysis I (chair: Cesare Tinelli)
  • Francesco Alberti, Silvio Ghilardi and Natasha Sharygina. Decision Procedures for Flat Array Properties
  • Alessandro Armando, Roberto Carbone and Luca Compagna. SATMC: a SAT-based Model Checker for Security-critical Systems
  • Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta. IC3 Modulo Theories via Implicit Predicate Abstraction
  • Hassan Eldib, Chao Wang and Patrick Schaumont. SMT-Based Verification of Software Countermeasures against Side-Channel Attacks
12h30 - 14h00 Lunch
14h00 - 16h00 CC / Room: Mont Blanc
Parallelism and Parsing (chair: Amitabha Sanyal)
  • Paul Feautrier, Éric Violard and Alain Ketterlin. Improving X10 Program Performance by Clock Removal (25mn)
  • Jayvant Anantpur and Govindarajan R. Taming Control Divergence in GPUs through Control Flow Linearization (25mn)
  • Zheng Wang, Daniel Powell, Bjoern Franke and Michael O'Boyle. Exploitation of GPUs for the Parallelisation of Probably Parallel Legacy Code (25mn)
  • Martin Sulzmann and Pippijn van Steenhoven. A Flexible and Efficient ML Lexer Tool based on Extended Regular Expression Submatching (25mn)
  • Alessandro Barenghi, Stefano Crespi Reghizzi, Dino Mandrioli, Federica Panella and Matteo Pradella. The PAPAGENO parallel-parser generator (Tool presentation, 15mn)
POST / Room: Makalu
Quantitative Aspects of Information Flow (chair: Catuscia Palamidessi)
  • Annabelle McIver, Carroll Morgan, Geoffrey Smith, Barbara Espinoza and Larissa Meinicke. Abstract Channels and their Robust Information-leakage Ordering (nomination for best paper award)
  • Rohit Chadha, Dileep Kini and Mahesh Viswanathan. Quantitative Information Flow in Boolean Programs
  • Mario S. Alvim, Fred B. Schneider and Andre Scedrov. When not All Bits are Equal: Worth-based Information Flow
  • Florian Arnold, Holger Hermanns, Reza Pulungan and Marielle I A Stoelinga. Time-Dependent Analysis of Attacks
TACAS / Room: Amphitheater
Decision procedures and their application in analysis II (chair: Erika Abraham)
  • Bernd Finkbeiner and Leander Tentrup. Detecting Unrealizable Specifications of Distributed Systems
  • Arie Gurfinkel, Anton Belov and Joao Marques-Silva. Synthesizing Safe Bit-Precise Invariants
  • Michael Huth and Jim Huan-Pu Kuo. PEALT: An Automated Reasoning Tool for Numerical Aggregation of Trust Evidence
  • Ruzica Piskac, Thomas Wies and Damien Zufferey. GRASShopper: Complete Heap Verification with Mixed Specifications
16h00 - 16h30 Coffee Break
16h30 - 18h00 CC / Room: Mont Blanc
New Trends in Compilation (chair: Henri-Pierre Charles)
  • Magnus Madsen and Esben Andreasen. String Analysis for Dynamic Field Access (25mn)
  • Rafael Auler, Edson Borin, Peli de Halleux, Michal Moskal and Nikolai Tillmann. Addressing JavaScript JIT engines performance quirks: A crowdsourced adaptive compiler (25mn)
  • Thomas M. Prinz, Norbert Spieß and Wolfram Amme. A First Step Towards a Compiler for Business Processes (Tool presentation, 15mn)
  • Martin Franz, Andreas Holzer, Stefan Katzenbeisser, Christian Schallhart and Helmut Veith. CBMC-GC: An ANSI C Compiler for Secure Two-Party Computations (Tool presentation, 15mn)
POST / Room: Makalu
Information Flow Control in Programming Languages (chair: Pierpaolo Degano)
  • Abhishek Bichhawat, Vineet Rajani, Deepak Garg and Christian Hammer. Information Flow Control in WebKit’s JavaScript Bytecode
  • David Costanzo and Zhong Shao. A Separation Logic for Enforcing Declarative Information Flow Control Policies
  • Jed Liu and Andrew Myers. Defining and Enforcing Referential Security
TACAS / Room: Amphitheater
Complexity and termination analysis (chair: Lenore Zuck)
  • Marc Brockschmidt, Fabian Emmes, Stephan Falke, Carsten Fuhs and Jürgen Giesl. Alternating Runtime and Size Complexity Analysis of Integer Programs
  • Hong-Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar and Peter O'Hearn. Proving Nontermination via Safety
  • Jan Leike and Matthias Heizmann. Ranking Function Templates for Linear Loops
19h30 - 22h00
Reception at Musée de Grenoble