| 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 |