ETAPS 2015 Workshops Programme

• 09h30: Introduction
• 09h45: Pierre-Louis Curien (special session)

• 11h00: Luke Ong (special session)
• 11h45: Samson Abramsky (special session)

• 14h00: Andrzej Murawski (tutorial)
• 14h30: Ugo Dal Lago, Claudia Faggian, Benoît Valiron and Akira Yoshimizu. Parallelism and Synchronization in an Infinitary Context
• 15h00: Yann Hamdaoui. Multitoken Geometry of Interaction and Multimove Games
• 15h30: Simon Castellan. A game semantics for fork(II)

• 16h30: Charles Grellois and Paul-André Melliès. Coloured tensorial logic and higher-order model-checking
• 17h00: Colin Riba. Some Monoidal Fibrations of Tree Automata
• 17h30: Clément Jacq and Paul-André Melliès. Distributive laws and finitary Game Semantics of Linear Logic

• NO MORNING SESSION

• 14h00: Alexander Heußner, Christopher M. Poskitt, Claudio Corrodi and Benjanim Morandi. Towards Practical Graph-Based Verification for an Object-Oriented Concurrency Model
  
• 14h30: Detlef Plump, Christopher Bak, Glyn Faulkner and Colin Runciman. A Reference Interpreter for the Graph Programming Language GP
• 15h00: Géza Kulcsár, Frederik Deckwerth, Malte Lochau, Gergely Varro and Andy Schürr. Improved Conflict Detection for Graph Transformation with Attributes
• 15h30: Marwan Radwan and Reiko Heckel. Detecting and Refactoring Operational Smells within the Domain Name System

• 16h30: TOOL DEMOS

• 09h30: Catuscia Palamidessi (invited speaker)

• 11h00: Fabio Martinelli, Ilaria Matteucci and Francesco Santini. Semiring-based Specification Approaches for Quantitative Security
• 11h30: 12:00 Rajesh Kumar, Dennis Guck and Marielle Stoelinga. Time Dependent Analysis with Dynamic Counter Measure Trees
• 12h00: Yusuke Kawamoto and Thomas Given-Wilson. Quantitative Information Flow for Scheduler-Dependent Systems

• 14h30: Matias David Lee and Erik de Vink. Rooted probabilistic branching bisimulation as a congruence 
• 15h00: Diego Latella, Mieke Massink and Erik De Vink. A Definition Scheme for Quantitative Bisimulation
• 15h30: Alessandro Aldini and Marco Bernardo. Expected-Delay-Summing Weak Bisimilarity for Markov Automata

• 16h30: Luca Bortolussi and Jane Hillston. Efficient Checking of Individual Rewards Properties in Markov Population Models
• 17h00: Arnd Hartmanns and Holger Hermanns. Explicit Model Checking of Very Large MDP using Partitioning and Secondary Storage

• 09h30: Kevin Hammond. Structure, Semantics and Speedup: Reasoning about Structured Parallel Programs using Dependent Types (invited speaker) [TACLe session 9h30-12h30]

• 11h00: Elvira Albert, Antonio E. Flores Montoya and Samir Genaim. May-Happen-in-Parallel Analysis with Condition Synchronization
• 11h30: Bernard van Gastel, Rody Kersten and Marko van Eekelen. A Dependent Type System for Energy Consumption Analysis
• 12h00: Emmanuel Hainry and Romain Péchoux. Implicit computational complexity in Object Oriented Programs

• 14h30: Martin Avanzini, Ugo Dal Lago and Georg Moser. Higher-Order Complexity Analysis: Harnessing First-Order Tools
• 15h00: Emmanuel Hainry and Romain Péchoux. Higher order interpretations for Basic Feasible Functions
• 15h30: Dominic Orchard. Complexity bounds from abstract categorical models

• 16h30: Jakob Grue Simonsen. Cons-free Term Rewriting and Complexity Classes (invited speaker)

• Parosh Abdulla. Cut-offs in Parameterized Verification (invited talk)

• 11h00: Benoit Delahaye. Consistency for Parametric Interval Markov Chains
• 11h30: Laurent Fribourg, Ulrich Kühne and Nicolas Markey. Game-based Synthesis of Distributed Controllers for Sampled Switched Systems
• 12h00: Adrien Le Coent, Florian De Vuyst, Christian Rey, Ludovic Chamoin and Laurent Fribourg. Guaranteed control of switched control systems using model order reduction and state-space bisection

• 14h00: Marta Kwiatkowska. Parameter synthesis for probabilistic real-time systems (invited talk)
• 15h00: Bharath Siva Kumar Tati and Markus Siegle. Parameter and Controller Synthesis for Markov Chains with Actions and State Labels
• 15h30: Peter Christoffersen, Mikkel Hansen, Anders Mariegaard, Julian T. Ringsmose, Kim G. Larsen and Radu Mardare. Parametric Verification of Weighted Systems

• 16h30: Julien Alexandre Dit Sandretto, Alexandre Chapoutot and Olivier Mullier. Tuning PI controller in nonlinear uncertain closed-loop systems with interval analysis
  
  
• Informal Presentations:
• 17h00: Nicolas David, Claude Jard, Didier Lime, and Olivier H. Roux. Discrete Parameters in Petri Nets (accepted at Petri Nets 2015)
• 17h20: Hoang Gia Nguyen. Enhanced Distributed Behavioral Cartography of Timed Automata (under submission)
• 17h40: Alessandro Cimatti, Alberto Griggio, Sergio Mover and Stefano Tonetta. Parameter Synthesis with IC3 (presented at FMCAD 2013)

• 09h15: Welcome
• 09h30: Marsha Chechik. Towards a Framework for Managing Software Families (invited talk)
  

• 11h00: Lars Luthmann, Stephan Mennicke and Malte Lochau. Towards an I/O Conformance Testing Theory for Software Product Lines based on Modal Interface Automata
• 11h30: Tessa Belder, Maurice H. Ter Beek and Erik De Vink. Coherent branching feature bisimulation
• 12h00: Uwe Lesta, Ina Schaefer and Tim Winkelmann. Detecting and Explaining Conflicts in Attributed Feature Models

• 14h00: Thi-Kim-Zung Pham, Catherine Dubois and Nicole Levy. Towards correct-by-construction product variants of a software product line: GFML, a formal language for feature modules
• 14h30: Maurice H. Ter Beek, Axel Legay, Alberto Lluch Lafuente and Andrea Vandin. Quantitative Analysis of Probabilistic Software Product Line Models with Statistical Model Checking
• 15h00: Ian Peake, Jan Olaf Blech, Lasith Fernando, Divyasheel Sharma, Srini Ramaswamy and Mallikarjun Kande. Analysis of Software Binaries for Reengineering-Driven Product Line Architecture – An Industrial Case Study
• 15h30: Discussion

• Panel discussion
  

• 09h00: Opening
  
• 09h15: Arie Gurfinkel (Carnegie Mellon University, USA). The SeaHorn Verification Framework (invited talk) 
• 10h00: Martin Lester. Control Flow Analysis for SF Combinator Calculus

• 11h00: Bishoksan Kafle, John P. Gallagher and Pierre Ganty. Decomposition by Tree Dimension in Horn Clause Verification
• 11h30: G.W. Hamilton. Verifying Temporal Properties of Reactive Systems by Transformation
• 12h00: Discussion

• 14h00: David Monniaux (VERIMAG, CNRS - University of Grenoble, France). Program Transformation and Verification are Interrelated (invited talk)
• 14h45: Emanuele De Angelis, Fabio Fioravanti, Alberto Pettorossi and Maurizio Proietti. Proving Horn Clause Specifications of Imperative Programs
• 15h15: Wei Bai and Emmanuel M. Tadjouddine. Automated Program Translation in Certifying Online Auctions
• 15h45: Discussion

• 16h30: Alexei P. Lisitsa and Andrei P. Nemytykh. Finite Countermodel Based Verification for Program Transformation (A Case Study)
• 17h00: Sebastian Schlesinger, Paula Herber, Thomas Gothel and Sabine Glesner. Towards the Verification of Refactorings of Hybrid Simulink Models (Presentation)
• 17h20: Fouad ben Nasr Omri, Safa Omri and Ralf Reussner. Incremental and Compositional Probabilistic Analysis of Programs under Uncertainty. (Presentation)
• 17h40h: Discussion

• 09h00: Paul Blain Levy (invited talk)
• 10h00: James Laird. Game Semantics for Bounded Polymorphism

• 11h00: Christophe Fouquere and Myriam Quatrini. A Characterization of Ludics in Game Semantics
• 11h30: Alice Pavaux. Internal Completeness in Nonlinear Ludics
• 12h00: David Baelde, Amina Doumane and Alexis Saurin. Least and Greatest Fixed Points in Ludics

• 14h00: Nikos Tzevelekos (invited talk)
• 15h00: Guilhem Jaber. Reasoning on Equivalence of Stateful Programs: A Marriage of Game Semantics and Operational Techniques
• 15h30: Dietmar Berwanger and Marie Van Den Bogaard. Caring but not knowing. On preplay communication in infinite games

• 16h30: Valentin Blot. Positional interpretation of Peano arithmetic with winning strategies
• 17h00: Étienne Miquey. Realizability games for arithmetical formulæ
• 17h30: Can Baskent. Game Semantics: A Paraconsistent Approach

• 09h00: Heinz Ulrich Hoppe. Network Analysis of Online Communities - Applications and Tools (invited speaker)
• 10h00: Anton Wijs. Confluence Detection for Transformations of Labelled Transition Systems.

• 11h00: Luc Moreau. Aggregation by Provenance Types: A Technique for Summarising Provenance Graphs
• 11h30: Jason Vallet, Bruno Pinaud, Guy Melançon and Hélène Kirchner. A Visual Analytic Approach to Compare Propagation Models in Social Networks
• 12h00: Aleks Kissinger and Vladimir Zamdzhiev. !-graphs with Trivial Overlap are Context-free

• 14h00: Ugo Montanari, Matteo Sammartino and Nicklas Hoch. Dynamic Programming on Nominal Graphs
• 14h30: Discussion Groups

• 16h30: Discussion Talks
  
• 17h00: Challenges Session
  

• 09h30: Holger Hermanns (invited speaker)

• 11h00: TBC (invited speaker)
• 11h30: CARMA: Collective Adaptive Resource-sharing Markovian Agents
• 12h00: Mads Rosendahl and Maja Kirkeby. Probabilistic Output Analysis by Program Manipulation

• 09h30: Simona Ronchi Della Rocca. Intersection Types and Implicit Computational Complexity 
• (invited talk)

• 11h00: Guillaume Bonfante, Jean-Yves Moyen and Pierre Boudes. Extensional filters reveal algorithms
• 11h30: Pierre Valarcher and Yoann Marquer. An algorithmic complete programming language for a large class of algorithms computable in polynomial time
• 12h00: Clément Aubert. An in-between “implicit” and “explicit” complexity: Automata

• 14h00: Thomas Seiller. Towards a Complexity-through-Realizability Theory
• 14h30: Reinhard Kahle and Isabel Oitavem. The probabilistic class PP
• 15h00: Patrick Baillot, Gilles Barthe and Ugo Dal Lago. Implicit Computational Complexity of Subrecursive Cryptographic Reductions
• 15h30: Jostein Aanderaa. On Robinson style simplifications to the traditional bounded recursion on notation scheme

• 16h30: Deepak Garg. Type-based analysis of incremental computational complexity (invited speaker)

• 09h00: Tristan Crolard, CNAM, France. A verified abstract machine for functional coroutines (invited talk)
• 10h00: Jules Hedges, Queen Mary University of London, UK. The selection monad as a CPS translation

• 11h00: Neil Sculthorpe, Paolo Torrini, and Peter Mosses, Swansea University, UK. A modular structural operational semantics for delimited continuations
• 11h30: Gabriel Kerneis, Paris, France. Why all programmers want continuations (but use callbacks instead) (distilled tutorial)

• 14h00: Hayo Thielecke, University of Birmingham, UK. Command injection attacks, continuations, and the Lambek calculus (distilled tutorial)
• 15h00: Serguei Lenglet, Université de Lorraine, France. Bisimulations for delimited-control operators (distilled tutorial)

• 16h30: Ikuo Kobori and Yukiyoshi Kameyama, University of Tsukuba, Japan; Oleg Kiselyov, Tohoku University, Japan. ATM without tears: prompt-passing style transformation for typed delimited-control operators
• 17h00: Jay McCarthy, Vassar College, USA. Theory and application of continuation marks (distilled tutorial)

• 09h00: Workshop opening
• 09h15: Steffen Zschaler (King's College London, UK). Building flexible analysis: Modular formal specification of QoS and QoS analysis (Invited talk)

• 11h00: Jean-Michel Hufflen. Using Model-Checking Techniques for Component-Based Systems with Reconfigurations
• 11h30: Nils Jähnig, Thomas Göthel and Sabine Glesner. A Denotational Semantics for Communicating Unstructured Code
• 12h00: Vasileios Koutsoumpas. A Formal Approach based on Fuzzy Logic for the Specification of Interactive Systems

• 14h00: Michael Langhammer (Karlsruhe Institute of Technology, Germany). Co-Evolution of Component-based Architecture and Code using Vitruvius (tutorial)
• 15h15: Panel Discussion (B. Buhnova, J. Kofron and L. Happe). Changing role of Software Architecture in Research and Development

• 16h30: Heinz Riener, Ruediger Ehlers and Goerschwin Fey. Path-Based Program Repair
• 16h55: Diego Marmsoler, Alexander Malkis and Jonas Eckhardt. A Model of Layered Architectures
• 17h20: Ian Cassar, Adrian Francalanza and Simon Said. Improving Runtime Overheads for detectEr
• 17h45: Workshop closing

• 09h00: Challenge 1
• 10h00: BREAK
• 10h15: Challenge 2
• 11h15: BREAK
• 11h30: Challenge 3

• Discussion & Judging

Francis Bancroft Building / Room: FB.1.13a

Session on programming language design

• 11h20: Opening
• 11h30: Avik Chaudhuri + Basil Hosmer (Facebook US). Flow
• 12h00: Dulma Rodríguez (Facebook UK). Static analysis at Facebook

Francis Bancroft Building / Room: FB.1.13a

Session on using programming languages in software development companies

• 14h00: Michael Sperber (Active Group GmbH). Functional Programming
• 14h30: Uri Baghin (Facebook UK). Source Control and Building at Facebook
• 15h00: Tyler Sorensen (UCL). GPU Concurrency: Weak Behaviour and Programming Assumptions
• 15h30: Fausto Spoto (Juliasoft). Experience with the Static Analysis of Banking and Insurance Java code with Julia

Francis Bancroft Building / Room: FB.1.13a

• 16h30: Don Syme (Microsoft). The F# Path to Relaxation

• Emiliano De Cristofaro. The Genomics Revolution: Innovation Dream or Privacy Nightmare? (invited speaker, joint with TPDP)

• 10h00: Dimitrios Kouzapas and Anna Philippou. Type checking privacy policies in the pi-calculus

• 11h00: Ximeng Li, Flemming Nielson and Hanne Riis Nielson. Factorization of Behavioral Integrity
• 11h30: Michael Backes, Esfandiar Mohammadi and Tim Ruffing. Computational Soundness for Interactive Primitives for Equivalence Properties
• 12h00: Ben Smyth and David Bernhard. Ballot secrecy with malicious bulletin boards

• 14h00: Cas Cremers. Symbolic security protocol analysis using the Tamarin Prover (invited talk)
• 15h00: Sreekanth Malladi. Towards a completeness result for model-checking of modern-day security protocols
• 15h30: Johannes Kinder. Hypertesting: The Case for Automated Testing of Hyperproperties

• 16h30: Jason Crampton, Charles Morisset and Nicola Zannone. Access Control with Non-deterministic and Probabilistic Attribute Retrieval
• 17h00: Umbreen Sabir Mian, Jerry Den Hartog, Sandro Etalle and Nicola Zannone. Auditing with incomplete logs

• WG 1.7 business meeting