ETAPS 2016 Programme Monday - Thursday

Monday 4 April

Room: Blauwe Zaal
ETAPS Opening: Joost-Pieter Katoen (RWTH Aachen University, Germany)
The slides are available here.

Room: Blauwe Zaal (Chair: Joost-Pieter Katoen)
Unifying Invited Talk: Andrew Gordon (MSR Cambridge and University of Edinburgh, UK)

Structure and Interpretation of Probabilistic Programs

Abstract: Probabilistic programming is a technique for solving statistical inference and machine learning problems by writing short pieces of code to model data. We survey the area and describe recent advances in semantic interpretation. Probabilistic programs exhibit structures that include hierarchies of random variables corresponding to the data schema, recurring modelling patterns, and also the classical Bayesian distinction between prior and likelihood. We exploit this structure in language designs that yield data insights with only a modicum of user input.

• Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt and Alexandra Silva. Probabilistic NetKAT
• Andreas Lochbihler. Probabilistic functions and cryptographic oracles in higher order logic
• Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja and Federico Olmedo. Weakest precondition reasoning for expected run-times of probabilistic programs (EATCS award nominee)
• Daniel Huang and Greg Morrisett. An application of computable distributions to the semantics of probabilistic programming languages (EAPLS award nominee)

• Neil Ghani, Fredrik Nordvall Forsberg and Alex Simpson. Comprehensive parametric polymorphism: categorical models and type theory (EATCS award nominee)
• Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Lars Birkedal and Rasmus Ejlers Møgelberg. Guarded Dependent Type Theory with Coinductive Types
• Danel Ahman, Neil Ghani and Gordon Plotkin. Dependent Types and Fibred Computational Effects
• James Laird. Game Semantics for Bounded Polymorphism

• Thomas Schmitz, Dustin Rhodes, Cormac Flanagan, Thomas Austin and Kenneth Knowles. Faceted Information Flow in Haskell via Control and Data Monads
• Iulia Bolosteanu and Deepak Garg. Asymmetric Secure Multi-execution with Declassification
• Nataliia Bielova and Tamara Rezk. A Taxonomy of Information Flow Monitors
• Joachim Breitner, Juergen Graf, Martin Hecker, Martin Mohr and Gregor Snelting. On Improvements Of Low-Deterministic Security
• [Tool demo] Juergen Graf, Martin Hecker, Martin Mohr and Gregor Snelting. Tool Demonstration: JOANA

• Alexey Bakhirkin and Nir Piterman. Finding Recurrent Sets with Backwards Analysis and Trace Partitioning
• Gudmund Grov and Vytautas Tumas. Tactics for the Dafny Program Verifier (EASST award nominee)
• Caterina Urban, Arie Gurfinkel and Temesghen Kahsai. Synthesizing Ranking Functions from Bits and Pieces
• Radu Iosif, Adam Rogalewicz and Tomas Vojnar. Abstraction Refinement and Antichains for Trace Inclusion of Infinite State Systems

• Steven Keuchel, Stephanie Weirich and Tom Schrijvers. Needle & knot: binder boilerplate tied up
• Richard A. Eisenberg, Stephanie Weirich and Hamidhasan Ahmed. Visible type application
• Alejandro Serrano and Jurriaan Hage. Type error diagnosis for embedded DSLs by two-stage specialized type rules
• Ambrose Bonnaire-Sergeant, Sam Tobin-Hochstadt and Rowan Davies. Practical optional types for Clojure

• Holger Bock Axelsen and Robin Kaarsgaard. Join Inverse Categories as Models of Reversible Recursion
• Venanzio Capretta and Tarmo Uustalu. A Coalgebraic View of Bar Recursion and Bar Induction
• Stefan Milius, Dirk Pattinson and Thorsten Wimann. A New Foundation for Finitary Corecursion
• Silvio Ghilardi, Maria João Gouveia and Luigi Santocanale. Fixed-point elimination in the Intuitionistic Propositional Calculus

• Quoc Huy Do, Nathan Wasser and Eduard Kamburjan. Towards Fully Automatic Logic-Based Information Flow Analysis: An Electronic-Voting Case Study
• Kevin Falzon and Eric Bodden. Towards a Comprehensive Model of Isolation for Mitigating Illicit Channels
• Sepehr Amir-Mohammadian, Stephen Chong and Christian Skalka. Correct Audit Logging: Theory and Practice
• Holger Hermanns, Julia Krämer, Jan Krcal and Marielle Stoelinga. The Value of Attack-Defence Diagrams

• Luca Cardelli, Mirco Tribastone, Max Tschaikowski and Andrea Vandin. Efficient Syntax-driven Lumping of Differential Equations
• Przemysław Daca, Thomas Henzinger, Jan Křetínský and Tatjana Petrov. Faster Statistical Model Checking for Unbounded Temporal Properties (EATCS award nominee)
• Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu and Joost-Pieter Katoen. Safety-constrained Reinforcement Learning for MDPs
• Sadegh Soudjani, Rupak Majumdar and Alessandro Abate. Safety Verification of Continuous-Space Pure Jump Markov Processes

The Design and Analysis of End-to End Verifiable Voting Systems

• Christof Löding, Parthasarathy Madhusudan and Daniel Neider. Abstract Learning Frameworks for Synthesis
• Parthasarathy Madhusudan, Daniel Neider and Shambwaditya Saha. Synthesizing Piece-wise Functions by Learning Classifiers (EASST award nominee)
• Daniel Neider and Ufuk Topcu. An Automaton Learning Approach to Solving Safety Games over Infinite Graphs

Reception at Kazerne (Paradijslaan 2-8)
(map / directions)

Tuesday 5 April

Room: Blauwe Zaal (Chair: Luca Viganò)
POST Invited Talk: Vitaly Shmatikov (Cornell Tech, USA)

Machine Learning and Privacy: Friends or Foes?

Abstract: Machine learning is eating the world. Modern machine learning methods, especially deep learning based on artificial neural networks, rely on the training data collected from millions of users to achieve unprecedented accuracy and enable powerful AI-based services.
In this talk, I will discuss the complex relationship between machine learning and digital privacy. This includes new threats, such as adversarial use of machine learning to recover hidden user data, and new benefits, such as privacy-preserving machine learning that protects the confidentiality of training data while constructing accurate models.

• Samik Basu and Tevfik Bultan. Automated Choreography Repair
• Claudio Corrodi, Alexander Heußner and Christopher M. Poskitt. A Graph-Based Semantics Workbench for Concurrent Asynchronous Programs
• Jia-Chun Lin, Ingrid Yu, Einar Broch Johnsen and Ming-Chang Lee. ABS-YARN: A Formal Framework for Modeling Hadoop YARN Clusters
• Ludovic Henrio, Oleksandra Kulankhina, Siqi Li and Eric Madelaine. Integrated environment for verifying and running distributed components

• Adrian Francalanza. A Theory of Monitors (Extended Abstract)
• Ranko Lazic and Andrzej Murawski. Contextual approximation and higher-order procedures
• Torben Amtoft and Anindya Banerjee. A Theory of Slicing for Probabilistic Control Flow Graphs
• Paul Gastin and Marie Fortin. Verification of parameterized communicating automata via split-width

• Matthew Bauer, Rohit Chadha and Mahesh Viswanathan. Composing protocols with randomized actions
• Veronique Cortier, Antoine Dallon and Stephanie Delaune. Bounding the number of agents, for equivalence too (EASST and EATCS award nominee)
• Sebastian A. Mödersheim and Alessandro Bruni. AIF-omega: Set-Based Protocol Abstraction with Countable Families
• Jian Xiong Shao, Yu Qin and Dengguo Feng. Computational Soundness Results for Stateful Applied pi Calculus (EAPLS award nominee)

• Olivier Bouissou, Eric Goubault, Sylvie Putot, Aleksandar Chakarov and Sriram Sankaranarayanan. Uncertainty Propagation using Probabilistic Affine Forms and Concentration of Measure Inequalities
• Kim G. Larsen, Marius Mikucionis, Marco Muniz, Jiri Srba and Jakob Haahr Taankvist. Online and Compositional Learning of Controllers with Application to Floor Heating
• Aleksandar Chakarov, Yuen-Lam Voronin and Sriram Sankaranarayanan. Deductive Proofs of Almost Sure Persistence and Recurrence Properties
• Rayna Dimitrova, Luis María Ferrer Fioriti, Holger Hermanns and Rupak Majumdar. Probabilistic CTL* : The Deductive Way

Room: Blauwe Zaal (Chair: Peter Thiemann)
ESOP Invited Talk: Cristina Lopes (University of California at Irvine, USA)

Simulating Cities: A Software Engineering Perspective

Abstract: Despite all the reasons why complex simulations are desirable for decision and policy making, and despite advances in computing power, large distributed simulations of urban areas are still rarely used, with most of their adoption in military applications. The reality is that developing distributed simulations is much harder than developing non-distributed, specialized ones, and requires a much higher level of software engineering expertise.
This talk looks at urban simulations from a software engineering and systems design perspective, and puts forward the idea that non-traditional decompositions in simulation load management are not just beneficial for these applications, but are likely the only way to move that field forward.

• Tony Garnock-Jones and Matthias Felleisen. Coordinated concurrent programming in Syndicate
• Christopher Schuster, Tim Disney and Cormac Flanagan. Macrofication: refactoring by reverse macro expansion
• Yuting Wang and Gopalan Nadathur. The higher-order abstract syntax approach to verified transformations on functional programs
• Hideyuki Kawabata and Hideya Iwasaki. Improving floating-point numbers: a lazy approach to adaptive accuracy refinement for numerical computations
• Nicolas Feltman, Kayvon Fatahalian, Umut Acar and Carlo Angiuli. Automatically splitting a two-stage lambda calculus

• Romain Brenguier. Robust Equilibria in Mean-Payoff Games
• Theo Pierron, Thomas Place and Marc Zeitoun. Quantifier Alternation for Infinite Words
• Dmitry Chistikov, Pavel Martyugin and Mahsa Shirmohammadi. Synchronizing automata over nested words
• Normann Decker and Daniel Thoma. On Freeze LTL with Ordered Attributes
• Peter Habermehl and Antoine Durand-Gasselin. Regular transformations of data words through origin information

• Oszkár Semeráth, András Vörös and Dániel Varró. Iterative and incremental model generation by logic solvers
• Csaba Debreceni, István Ráth, Dániel Varró, Xabier De Carlos, Xabier Mendialdua and Salvador Trujillo. Automated Model Merge by Design Space Exploration
• Daniel Strüber, Julia Rubin, Thorsten Arendt, Marsha Chechik, Gabriele Taentzer and Jennifer Plöger. RuleMerger: Automatic Construction of Variability-Based Model Transformation Rules (EASST award nominee)
• Xabier De Carlos, Goiuria Sagardui and Salvador Trujillo. Two-Step Transformation of Model Traversal EOL Queries for Large CDO Repositories
• Markus Weckesser, Malte Lochau, Thomas Schnabel, Björn Richerzhagen and Andy Schürr. Mind the Gap! Automated Anomaly Detection for Potentially Unbounded Cardinality-based Feature Models

Room: Blauwe Zaal
Tools I (Chair: Dirk Beyer)

Room: Zwarte Doos
Tools II (Chair: Radu Mateescu)

Wednesday 6 April

Room: Blauwe Zaal (Chair: Perdita Stevens)
FASE Invited Talk: Oscar Nierstrasz (Universität Bern, Switzerland)

The Death of Object-Oriented Programming

Abstract: Modern software systems are increasingly long-lived. In order to gracefully evolve these systems as they address new requirements, developers need to navigate effectively between domain concepts and the code that addresses those domains. One of the original promises of object-orientation was that the same object-oriented models would be used throughout requirements analysis, design and implementation. Software systems today however are commonly constructed from a heterogeneous “language soup” of mainstream code and dedicated DSLs addressing a variety of application and technical domains. Has object-oriented programming outlived its purpose?
We argue that we need to rethink the original goals of object-orientation and their relevance for modern software development. We propose as a driving maxim, “Programming is Modeling,” and explore what this implies for programming languages, tools and environments. In particular, we argue that: (1) source code should serve not only to specify an implementation of a software system, but should encode a queryable and manipulable model of the application and technical domains concerned; (2) IDEs should exploit these domain models to enable inexpensive browsing, querying and analysis by developers; and (3) barriers between the code base, the running application, and the software ecosystem at large need to be broken down, and their connections exploited and monitored to support developers in comprehension and evolution tasks.

• Dimitrios Kouzapas, Jorge A. Pérez and Nobuko Yoshida. On the relative expressiveness of higher-order session processes
• Emile Bres, Rob Van Glabbeek and Peter Höfner. T-AWN: a timed process algebra for wireless networks
• Emanuele D'Osualdo and C.-H. Luke Ong. On hierarchical communication topologies in the pi-calculus
• Johannes Åman Pohjola and Joachim Parrow. The expressive power of monotonic parallel composition

• Nathanael Fijalkow, Stefan Kiefer and Mahsa Shirmohammadi. Trace Refinement in Labelled Markov Decision Processes
• Parosh Aziz Abdulla, Radu Ciobanu, Richard Mayr, Arnaud Sangnier and Jeremy Sproston. Qualitative Analysis of VASS-Induced MDPs
• Madnani Khushraj, Krishna S. and Paritosh Pandya. Metric Temporal Logic with Counting
• Holger Hermanns, Jan Krcal and Steen Vester. Distributed Synthesis in Continuous Time

• Jean-Christophe Léchenet, Nikolai Kosmatov and Pascale Le Gall. Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices
• Lei Wang, Han Li and Xinchen Wang. The Influences of Edge Instability on Change Propagation and Connectivity in Call Graphs
• Pauline Bolignano, Thomas Jensen and Vincent Siles. Modeling and Abstraction of Memory Management in a Hypervisor
• Ali Sajedi Badashian, Abram Hindle and Eleni Stroulia. Crowdsourced Bug Triaging: Leveraging Q&A resources for Bug Assignment

• Cédric Favre, Hagen Völzer and Peter Müller. Diagnostic Information for Control-Flow Analysis of Workflow Graphs (aka Free-ChoiceWorkflow Nets)
• Michael Blondin, Alain Finkel, Christoph Haase and Serge Haddad. Approaching the Coverability Problem Continuously (EATCS award nominee)
• Constantin Enea and Azadeh Farzan. On Atomicity in Presence of Non-atomic Writes
• Daniel Poetzl and Daniel Kroening. Formalizing and Checking Thread Refinement for Data-Race-Free Execution Models

• Scott Owens, Magnus O. Myreen, Ramana Kumar and Yong Kiam Tan. Functional big-step semantics
• Gregory Malecha and Jesper Bengtson. Easy and efficient automation through reflective tactics
• Cláudio Belo Lourenço, Maria João Frade and Jorge Sousa Pinto. Formalizing single-assignment program verification: an adaptation-complete approach
• Alexander J. Summers and Peter Müller. Actor services: modular verification of message passing programs

• Clément Aubert, Marc Bagnol and Thomas Seiller. Unary Resolution: Characterizing Ptime
• Kaustuv Chaudhuri, Sonia Marin and Lutz Strassburger. Focused and Synthetic Nested Sequents
• Michele Pagani, Christine Tasson and Lionel Vaux. Strong Normalizability as a Finiteness Structure via the Taylor Expansion of lambda-terms
• Delia Kesner. Reasoning about call-by-need by means of types

• Marcus Gerhold and Marielle Stoelinga. Model-Based Testing of Probabilistic Systems (EASST award nominee)
• Guoxin Su, Taolue Chen, Yuan Feng, David Rosenblum and P.S. Thiagarajan. An Iterative Decision-Making Scheme for Markov Decision Processes and Its Application to Self-Adaptive Systems
• Philipp Chrszon, Clemens Dubslaff, Sascha Klüppelholz and Christel Baier. Family-Based Modeling and Analysis for Probabilistic Systems – Featuring ProFeat (EAPLS award nominee)
• Francisco Durán, Antonio Moreno-Delgado and José María Álvarez. Statistical model-checking of domain-specific modeling languages

• Benjamin Bittner, Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Marco Gario, Alberto Griggio, Cristian Mattarei, Andrea Micheli and Gianni Zampedri. The xSAP Safety Analysis Platform
• Radu Calinescu, Kenneth Johnson and Colin Paterson. FACT: A Probabilistic Model Checker for Formal Verification with Confidence Intervals
• Sung-Shik T.Q. Jongmans and Farhad Arbab. PrDK: Protocol Programming with Automata
• Hugues Evrard. DLC: Compiling a Concurrent System Formal Specification to a Distributed Implementation
• Marta Kwiatkowska, David Parker and Clemens Wiltsche. PRISM-games 2.0: A Tool for Multi-Objective Strategy Synthesis for Stochastic Games
• Luca Compagna, Daniel Ricardo Dos Santos, Serena Elisa Ponta and Silvio Ranise. Cerberus: Automated Synthesis of Enforcement Mechanisms for Security-sensitive Business Processes
• Yuhui Lin, Pierre Le Bras and Gudmund Grov. Developing & Debugging Proof Strategies by Tinkering
• Rajdeep Mukherjee, Michael Tautschnig and Daniel Kroening. v2c - A Verilog to C Translator Tool

K: a semantic framework for programming languages and formal analysis tools

• Kedar S. Namjoshi and Richard J. Trefler. Parameterized Compositional Model Checking
• Jan Friso Groote and Anton Wijs. An O(m log n) Algorithm for Stuttering Equivalence and Branching Bisimulation
• Sicun Gao and Damien Zufferey. Interpolants in Nonlinear Theories over the Reals

Thursday 7 April

Room: Blauwe Zaal (Chair: Jean-François Raskin)
Unifying Invited Talk: Rupak Majumdar (MPI Kaiserslautern, Germany)

Robots at the Edge of the Cloud

Abstract: Computers have come a long way from their roots as fast calculating devices. We live in a world in which computers collect, store, and analyze huge volumes of data. We are seeing the beginnings of a new revolution in the use of computers. In addition to collecting and analyzing data, computers are influencing the physical world and interacting autonomously, and in complex ways, with large groups of humans. These cyber-physical-social systems have the potential to dramatically alter the way we lead our lives. However, designing these systems in a reliable way is a difficult problem. In this talk, we enumerate a set of research challenges that have to be overcome in order to realize the potential of cyber-physical-social systems.

• Pierre-Marie Pédrot and Alexis Saurin. Classical by-need
• Thomas Ehrhard. A functional language extending call-by-name and call-by-value, and its connection with linear logic
• Rodolphe Lepigre. A realizability model for a semantical value restriction
• Kasper Svendsen, Filip Sieczkowski and Lars Birkedal. Transfinite step-indexing: decoupling concrete and logical steps

• Piotr Hofman, Sławomir Lasota, Ranko Lazic, Jerõme Leroux, Sylvain Schmitz and Patrick Totzke. Coverability Trees for Petri Nets with Unordered Data
• Dmitry Chistikov, Wojciech Czerwiński, Piotr Hofman, Michał Pilipczuk and Michael Wehar. Shortest paths in one-counter systems
• Klaus Dräger. The Invariance Problem for Matrix Semigroups
• Jose Meseguer. Order-Sorted Rewriting and Congruence Closure

• David Aspinall, Cezary Kaliszyk. Proof Engineering Metrics
• Philipp Hoffmann and Javier Esparza. Reduction Rules for Colored Workflow Nets (EATCS award nominee)
• Claudia Elena Chiriță, José Luiz Fiadeiro and Fernando Orejas. Many-valued Institutions for Constraint Specification
• Adrian Riesco, Kazuhiro Ogata and Kokichi Futatsugi. CafeInMaude: a CafeOBJ interpreter in Maude

• Filip Konecny. PTIME Computation of Transitive Closures of Octagonal Relations
• Junkil Park, Miroslav Pajic, Insup Lee and Oleg Sokolsky. Scalable Verification of Linear Controller Software
• Pallavi Maiya, Rahul Gupta, Aditya Kanade and Rupak Majumdar. Partial Order Reduction for Event-driven Multi-threaded Programs
• Mohamed Faouzi Atig, K. Narayan Kumar and Prakash Saivasan. Acceleration in Multi-Pushdown systems

• Jacques Carette and Amr Sabry. Computing with semirings and weak rig groupoids
• Antoine Miné, Jason Breck and Thomas Reps. An algorithm inspired by constraint solvers to infer inductive invariants in numeric programs (EASST award nominee)
• Rajeev Alur, Dana Fisman and Mukund Raghothaman. Regular programming for quantitative properties of data streams
• Pedro Da Rocha Pinto, Thomas Dinsdale-Young, Philippa Gardner and Julian Sutherland. Modular termination verification for non-blocking concurrency

• Soichiro Fujii, Shin-ya Katsumata and Paul-André Melliès. Towards a formal theory of graded monads
• Liang-Ting Chen, Jiri Adámek, Stefan Milius and Henning Urbat. Profinite Monads, Profinite Equations and Reiterman's Theorem

TACAS / Room: CZ 7
Competition on Software Verification - Open Jury Meeting and Technical Discussion (Chair: Dirk Beyer) (starts at 15:00)

• Sander de Putter and Anton Wijs. Verifying a Verifier: On the Formal Correctness of an LTS Transformation Verification Technique
• Raymond Hu and Nobuko Yoshida. Hybrid Session Verification through Endpoint API Generation
• Pavel Jancik, Leonardo Alt, Grigory Fedyukovich, Antti Hyvärinen, Jan Kofron and Natasha Sharygina. PVAIR: Partial Variable Assignment InterpolatoR

• Ricardo Almeida, Lukas Holik and Richard Mayr. Minimization of Nondeterministic Tree Automata
• Dogan Ulus, Thomas Ferrere, Eugene Asarin and Oded Maler. Online Timed Pattern Matching using Derivatives
• Nima Roohi, Pavithra Prabhakar and Mahesh Viswanathan. Hybridization based CEGAR for Hybrid Automata with Affine Dynamics
• František Blahoudek, Matthias Heizmann, Sven Schewe, Jan Strejček and Ming-Hsien Tsai. Complementing Semi-deterministic Büchi Automata

• Yongwang Zhao, David Sanan, Fuyuan Zhang and Yang Liu. Reasoning About Information Flow Security of Separation Kernels with Channel-based Communication
• Yaron Velner, Kalev Alpernas, Aurojit Panda, Alexander Rabinovich, Mooly Sagiv, Scott Shenker and Sharon Shoham. Some Complexity Results for Stateful Network Verification

• Julien Lange and Nobuko Yoshida. Characteristic Formulae for Session Type
• Alexander Nadel and Vadim Ryvchin. Bit-Vector Optimization
• Normann Decker, Jannis Harder, Torben Scheffel, Malte Schmitz and Daniel Thoma. Runtime Monitoring with Union-Find Structures