ETAPS 2017
2017 European Joint Conferences on Theory and Practice of Software (ETAPS)
Powered by
Conference Publishing Consulting
2017 European Joint Conferences on Theory and Practice of Software (ETAPS), April 22–29, 2017, Uppsala, Sweden

ETAPS 2017 – Proceedings

 Contents - Abstracts - Authors
Online Calendar - iCal File

ESOP

Probabilistic Programming
Tue, Apr 25, 14:00 - 16:00, Sal B

Commutative Semantics for Probabilistic Programming
Sam Staton
(University of Oxford, UK)
Publisher's Version Best-Paper Award Nominee Article: etaps17esop-id99-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_32
Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring
Ryan Culpepper and Andrew Cobb
(Northeastern University, USA)
Publisher's Version Best-Paper Award Nominee Article: etaps17esop-id115-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_14
Metric Reasoning About λ-Terms: The General Case
Raphaëlle Crubillé and Ugo Dal Lago
(University of Paris Diderot, France; University of Bologna, Italy)
Publisher's Version Article: etaps17esop-id131-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_13
Probabilistic Termination by Monadic Affine Sized Typing
Ugo Dal Lago and Charles Grellois
(University of Bologna, Italy; University of Paris Diderot, France)
Publisher's Version Article: etaps17esop-id87-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_15

Graph Rewriting
Wed, Apr 26, 09:00 - 10:00, Sal B

Confluence of Graph Rewriting with Interfaces
Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi
(ENS Lyon, France; University of Pisa, Italy; Radboud University Nijmegen, Netherlands; University of Southampton, UK; University College London, UK)
Publisher's Version Article: etaps17esop-id53-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_6
Incremental Update for Graph Rewriting
Pierre Boutillier, Thomas Ehrhard, and Jean Krivine
(Harvard Medical School, USA; University of Paris Diderot, France; CNRS, France; amp, France)
Publisher's Version Article: etaps17esop-id71-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_8

Concurrency
Wed, Apr 26, 10:30 - 12:30, Sal B

Abstract Specifications for Concurrent Maps
Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik, and Philippa Gardner
(Imperial College London, UK)
Publisher's Version Article: etaps17esop-id65-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_36
Caper - Automatic Verification for Fine-Grained Concurrency
Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, and Lars Birkedal
(Aarhus University, Denmark; Imperial College London, UK)
Publisher's Version Article: etaps17esop-id81-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_16
Observed Communication Semantics for Classical Processes
Robert Atkey
(University of Strathclyde, UK)
Publisher's Version Article: etaps17esop-id72-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_3
Tackling Real-Life Relaxed Concurrency with FSL++
Marko Doko and Viktor Vafeiadis
(MPI-SWS, Germany)
Publisher's Version Article: etaps17esop-id63-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_17

Language Design
Wed, Apr 26, 14:00 - 16:00, Sal B

APLicative Programming with Naperian Functors
Jeremy Gibbons
(University of Oxford, UK)
Publisher's Version Article: etaps17esop-id6-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_21
Disjoint Polymorphism
João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi
(University of Hong Kong, China)
Publisher's Version Article: etaps17esop-id123-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_1
Extensible Datasort Refinements
Joshua Dunfield
(University of British Columbia, Canada)
Publisher's Version Article: etaps17esop-id97-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_18
The Essence of Functional Programming on Semantic Data
Martin Leinberger, Ralf Lämmel, and Steffen Staab
(University of Koblenz-Landau, Germany; University of Southampton, UK)
Publisher's Version Article: etaps17esop-id39-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_28

Verification
Wed, Apr 26, 16:30 - 18:00, Sal B

Is Your Software on Dope? Formal Analysis of Surreptitiously "enhanced" Programs
Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, and Holger Hermanns
(Universidad Nacional de Córdoba, Argentina; CONICET, Argentina; Saarland University, Germany; IMDEA Software Institute, Spain)
Publisher's Version Article: etaps17esop-id62-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_4
Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
Tim Wood, Sophia Drossopolou, Shuvendu K. Lahiri, and Susan Eisenbach
(Imperial College London, UK; Microsoft Research, USA)
Publisher's Version Article: etaps17esop-id105-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_35
Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, and Serdar Tasiran
(University of Paris Diderot, France; Nokia Bell Labs, USA; Koç University, Turkey)
Publisher's Version Article: etaps17esop-id82-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_7

Automated Verification
Thu, Apr 27, 10:30 - 12:30, Sal B

Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization
Hao Tang, Di Wang, Yingfei Xiong, Lingming Zhang, Xiaoyin Wang, and Lu Zhang
(Peking University, China; University of Texas at Dallas, USA; University of Texas at San Antonio, USA)
Publisher's Version Article: etaps17esop-id40-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_33
Faster Algorithms for Weighted Recursive State Machines
Krishnendu Chatterjee, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis
(IST Austria, Austria; IIT Bombay, India)
Publisher's Version Article: etaps17esop-id21-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_11
ML and Extended Branching VASS
Conrad Cotton-Barratt, Andrzej S. Murawski, and C.-H. Luke Ong
(University of Oxford, UK; University of Warwick, UK)
Publisher's Version Article: etaps17esop-id50-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_12
Modular Verification of Higher-Order Functional Programs
Ryosuke Sato and Naoki Kobayashi
(University of Tokyo, Japan)
Publisher's Version Article: etaps17esop-id129-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_31

Theorem Proving
Thu, Apr 27, 14:00 - 16:00, Sal B

Comprehending Isabelle/HOL's Consistency
Ondřej Kunčar and Andrei Popescu
(TU Munich, Germany; Middlesex University, UK)
Publisher's Version Article: etaps17esop-id31-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_27
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants
Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel
(Inria, France; LORIA, France; Max Planck Institute for Informatics, Germany; École Polytechnique, France; ETH Zurich, Switzerland; Middlesex University, UK)
Publisher's Version Article: etaps17esop-id26-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_5
Generalizing Inference Systems by Coaxioms
Davide Ancona, Francesco Dagnino, and Elena Zucca
(University of Genoa, Italy)
Publisher's Version Article: etaps17esop-id12-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_2
Verified Characteristic Formulae for CakeML
Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, and Michael Norrish
(ENS Lyon, France; Chalmers University of Technology, Sweden; Data61 at CSIRO, Australia)
Publisher's Version Article: etaps17esop-id80-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_22

Separation Logic
Fri, Apr 28, 10:30 - 12:30, Sal B

A Higher-Order Logic for Concurrent Termination-Preserving Refinement
Joseph Tassarotti, Ralf Jung, and Robert Harper
(Carnegie Mellon University, USA; MPI-SWS, Germany)
Publisher's Version Article: etaps17esop-id98-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_34
Temporary Read-Only Permissions for Separation Logic
Arthur Charguéraud and François Pottier
(Inria, France)
Publisher's Version Article: etaps17esop-id67-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_10
The Essence of Higher-Order Concurrent Separation Logic
Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal
(Delft University of Technology, Netherlands; MPI-SWS, Germany; Aarhus University, Denmark)
Publisher's Version Article: etaps17esop-id73-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_26
Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, and Florian Zuleger
(RWTH Aachen University, Germany; Vienna University of Technology, Austria)
Publisher's Version Article: etaps17esop-id54-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_23

Session Types
Fri, Apr 28, 14:00 - 16:00, Sal B

Context-Free Session Type Inference
Luca Padovani
(University of Turin, Italy)
Publisher's Version Best-Paper Award Nominee Article: etaps17esop-id76-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_30
Linearity, Control Effects, and Behavioural Types
Luis Caires and Jorge A. Pérez
(Nova University of Lisbon, Portugal; University of Groningen, Netherlands)
Publisher's Version Article: etaps17esop-id47-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_9
Proving Linearizability Using Partial Orders
Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew J. Parkinson
(IMDEA Software Institute, Spain; University of York, UK; Microsoft Research, UK)
Publisher's Version Article: etaps17esop-id45-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_24
The Power of Non-determinism in Higher-Order Implicit Complexity - Characterising Complexity Classes Using Non-deterministic Cons-Free Programming
Cynthia Kop and Jakob Grue Simonsen
(University of Copenhagen, Denmark)
Publisher's Version Article: etaps17esop-id77-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_25

Type Theory
Fri, Apr 28, 16:30 - 18:00, Sal B

A Classical Sequent Calculus with Dependent Types
Étienne Miquey
(Inria, France; IRIF, France; University of Paris Diderot, France; University of the Republic, Uruguay)
Publisher's Version Article: etaps17esop-id1-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_29
Lincx: A Linear Logical Framework with First-Class Contexts
Aina Linn Georges, Agata Murawska, Shawn Otis, and Brigitte Pientka
(McGill University, Canada; IT University of Copenhagen, Denmark)
Publisher's Version Article: etaps17esop-id30-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_20
Programs Using Syntax with First-Class Binders
Francisco Ferreira and Brigitte Pientka
(McGill University, Canada)
Publisher's Version Article: etaps17esop-id13-p doi:http://dx.doi.org/10.1007/978-3-662-54434-1_19

FASE

Learning and Inference
Wed, Apr 26, 09:00 - 10:00, K3+K4

Should We Learn Probabilistic Models for Model Checking? A New Approach and An Empirical Study
Jingyi Wang, Jun Sun, Qixia Yuan, and Jun Pang
(Singapore University of Technology and Design, Singapore; University of Luxembourg, Luxembourg)
Publisher's Version Article: etaps17fase-faseid1-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_1
Bordeaux: A Tool for Thinking Outside the Box
Vajih Montaghami and Derek Rayside
(University of Waterloo, Canada)
Publisher's Version Article: etaps17fase-faseid95-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_2

Test Selection
Wed, Apr 26, 10:30 - 12:30, K3+K4

Bucketing Failing Tests via Symbolic Analysis
Van-Thuan Pham, Sakaar Khurana, Subhajit Roy, and Abhik Roychoudhury
(National University of Singapore, Singapore; IIT Kanpur, India; Microsoft, India)
Publisher's Version Article: etaps17fase-faseid7-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_3
Selective Bisection Debugging
Ripon Saha and Milos Gligoric
(Fujitsu Labs, USA; University of Texas at Austin, USA)
Publisher's Version Article: etaps17fase-faseid107-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_4
On the Effectiveness of Bug Predictors with Procedural Systems: A Quantitative Study
Cristiano Werner Araújo, Ingrid Nunes, and Daltro José Nunes
(Federal University of Rio Grande do Sul, Brazil)
Publisher's Version Article: etaps17fase-faseid60-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_5

Program and System Analysis
Thu, Apr 27, 10:30 - 12:30, K3+K4

Inference and Evolution of TypeScript Declaration Files
Erik Krogh Kristensen and Anders Møller
(Aarhus University, Denmark)
Publisher's Version Best-Paper Award Nominee Article: etaps17fase-faseid14-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_6
Explicit Connection Actions in Multiparty Session Types
Raymond Hu and Nobuko Yoshida
(Imperial College London, UK)
Publisher's Version Article: etaps17fase-faseid17-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_7
Change and Delay Contracts for Hybrid System Component Verification
Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, and André Platzer
(JKU Linz, Austria; Carnegie Mellon University, USA)
Publisher's Version Article: etaps17fase-faseid68-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_8
Precise Version Control of Trees with Line-Based Version Control Systems
Dimitar Asenov, Balz Guenat, Peter Müller, and Martin Otth
(ETH Zurich, Switzerland; Ergon Informatik, Switzerland)
Publisher's Version Best-Paper Award Nominee Article: etaps17fase-faseid71-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_9

Graph Modelling and Transformation
Thu, Apr 27, 14:00 - 16:00, Sal C

StaticGen: Static Generation of UML Sequence Diagrams
Chris Alvin, Brian Peterson, and Supratik Mukhopadhyay
(Bradley University, USA; Louisiana State University, USA)
Publisher's Version Article: etaps17fase-faseid12-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_10
Inter-model Consistency Checking Using Triple Graph Grammars and Linear Optimization Techniques
Erhan Leblebici, Anthony Anjorin, and Andy Schürr
(TU Darmstadt, Germany; University of Paderborn, Germany)
Publisher's Version Article: etaps17fase-faseid23-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_11
GTS Families for the Flexible Composition of Graph Transformation Systems
Steffen Zschaler and Francisco Durán
(King's College London, UK; University of Málaga, Spain)
Publisher's Version Article: etaps17fase-faseid49-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_12
Symbolic Model Generation for Graph Properties
Sven Schneider, Leen Lambers, and Fernando Orejas
(HPI, Germany; Universitat Politècnica de Catalunya, Spain)
Publisher's Version Article: etaps17fase-faseid51-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_13

Model Transformations
Fri, Apr 28, 10:30 - 12:30, Sal C

Traceability Mappings as a Fundamental Instrument in Model Transformations
Zinovy Diskin, Abel Gómez, and Jordi Cabot
(McMaster University, Canada; University of Waterloo, Canada; Open University of Catalonia, Spain; ICREA, Spain)
Publisher's Version Article: etaps17fase-faseid50-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_14
Reusing Model Transformations Through Typing Requirement Models
Juan de Lara, Juri Di Rocco, Davide Di Ruscio, Esther Guerra, Ludovico Iovino, Alfonso Pierantonio, and Jesús Sánchez Cuadrado
(Autonomous University of Madrid, Spain; University of L'Aquila, Italy; Gran Sasso Science Institute, Italy)
Publisher's Version Article: etaps17fase-faseid54-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_15
Change-Preserving Model Repair
Gabriele Taentzer, Manuel Ohrndorf, Yngve Lamo, and Adrian Rutle
(University of Marburg, Germany; University of Siegen, Germany; Western Norway University of Applied Sciences, Norway)
Publisher's Version Article: etaps17fase-faseid74-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_16
A Deductive Approach for Fault Localization in ATL Model Transformations
Zheng Cheng and Massimo Tisi
(AtlanMod, France)
Publisher's Version Best-Paper Award Nominee Article: etaps17fase-faseid58-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_17

Configuration and Synthesis
Fri, Apr 28, 14:00 - 16:00, Sal C

OpenSAW: Open Security Analysis Workbench
Noomene Ben Henda, Björn Johansson, Patrik Lantz, Karl Norrman, Pasi Saarinen, and Oskar Segersvärd
(Ericsson Research, Sweden; KTH, Sweden)
Publisher's Version Article: etaps17fase-faseid87-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_18
Visual Configuration of Mobile Privacy Policies
Abdulbaki Aydin, David Piorkowski, Omer Tripp, Pietro Ferrara, and Marco Pistoia
(University of California at Santa Barbara, USA; IBM Research, USA; Google, USA; Julia, Italy)
Publisher's Version Article: etaps17fase-faseid97-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_19
Automated Workarounds from Java Program Specifications Based on SAT Solving
Marcelo Uva, Pablo Ponzio, Germán Regis, Nazareno Aguirre, and Marcelo F. Frias
(Universidad Nacional de Río Cuarto, Argentina; CONICET, Argentina; Buenos Aires Institute of Technology, Argentina)
Publisher's Version Article: etaps17fase-faseid103-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_20
Slicing from Formal Sematics: Chisel
Adrián Riesco, Irina Mariuca Asavoae, and Mihail Asavoae
(Complutense University of Madrid, Spain; Inria, France)
Publisher's Version Article: etaps17fase-faseid91-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_21
EasyInterface: A Toolkit for Rapid Development of GUIs for Research Prototype Tools
Jesús Doménech, Samir Genaim, Einar Broch Johnsen, and Rudolf Schlatte
(Complutense University of Madrid, Spain; University of Oslo, Norway)
Publisher's Version Article: etaps17fase-faseid47-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_22

Software Product Lines
Fri, Apr 28, 16:30 - 18:00, Sal C

Family-Based Model Checking with mCRL2
Maurice H. ter Beek, Erik P. de Vink, and Tim A. C. Willemse
(ISTI-CNR, Italy; Eindhoven University of Technology, Netherlands)
Publisher's Version Article: etaps17fase-faseid6-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_23
Variability-Specific Abstraction Refinement for Family-Based Model Checking
Aleksandar S. Dimovski and Andrzej Wąsowski
(IT University of Copenhagen, Denmark)
Publisher's Version Article: etaps17fase-faseid59-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_24
A Unified and Formal Programming Model for Deltas and Traits
Ferruccio Damiani, Reiner Hähnle, Eduard Kamburjan, and Michael Lienhardt
(University of Turin, Italy; TU Darmstadt, Germany)
Publisher's Version Article: etaps17fase-faseid94-p doi:http://dx.doi.org/10.1007/978-3-662-54494-5_25

FOSSACS

Coherence Spaces and Higher-Order Computation
Mon, Apr 24, 10:30 - 12:30, Sal B

Coherence Spaces and Uniform Continuity
Kei Matsumoto
(Kyoto University, Japan)
Publisher's Version Article: etaps17fossacs-fossacsid67-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_1
The Free Exponential Modality of Probabilistic Coherence Spaces
Raphaëlle Crubillé, Thomas Ehrhard, Michele Pagani, and Christine Tasson
(University of Paris Diderot, France)
Publisher's Version Article: etaps17fossacs-fossacsid32-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_2
From Qualitative to Quantitative Semantics - By Change of Base
James Laird
(University of Bath, UK)
Publisher's Version Article: etaps17fossacs-fossacsid95-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_3
Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence
Ryoma Sin'Ya, Kazuyuki Asada, Naoki Kobayashi, and Takeshi Tsukada
(University of Tokyo, Japan)
Publisher's Version Article: etaps17fossacs-fossacsid54-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_4

Algebra and Coalgebra
Mon, Apr 24, 14:00 - 16:00, Sal B

Algebra, Coalgebra, and Minimization in Polynomial Differential Equations
Michele Boreale
(University of Florence, Italy)
Publisher's Version Best-Paper Award Nominee Article: etaps17fossacs-fossacsid23-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_5
Equational Theories of Abnormal Termination Based on Kleene Algebra
Konstantinos Mamouras
(University of Pennsylvania, USA)
Publisher's Version Article: etaps17fossacs-fossacsid112-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_6
Companions, Codensity and Causality
Damien Pous and Jurriaan Rot
(CNRS, France; ENS Lyon, France; Radboud University Nijmegen, Netherlands)
Publisher's Version Article: etaps17fossacs-fossacsid82-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_7
Nominal Automata with Name Binding
Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann
(University of Erlangen-Nuremberg, Germany; Cornell University, USA)
Publisher's Version Article: etaps17fossacs-fossacsid50-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_8

Games and Automata
Tue, Apr 25, 10:30 - 12:30, Sal B

On the Existence of Weak Subgame Perfect Equilibria
Véronique Bruyère, Stéphane Le Roux, Arno Pauly, and Jean-Francois Raskin
(University of Mons, Belgium; Université Libre de Bruxelles, Belgium)
Publisher's Version Article: etaps17fossacs-fossacsid57-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_9
Optimal Reachability in Divergent Weighted Timed Games
Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier
(Aix-Marseille University, France; LIF, France; CNRS, France)
Publisher's Version Article: etaps17fossacs-fossacsid24-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_10
Bounding Average-Energy Games
Patricia Bouyer, Piotr Hofman, Nicolas Markey, Mickael Randour, and Martin Zimmermann
(CNRS, France; ENS Cachan, France; University of Paris-Saclay, France; IRISA, France; Inria, France; University of Rennes, France; Université Libre de Bruxelles, Belgium; Saarland University, Germany)
Publisher's Version Article: etaps17fossacs-fossacsid90-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_11
Logics of Repeating Values on Data Trees and Branching Counter Systems
Sergio Abriola, Diego Figueira, and Santiago Figueira
(University of Buenos Aires, Argentina; CNRS, France)
Publisher's Version Article: etaps17fossacs-fossacsid86-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_12

Automata, Logic, and Formal Languages
Tue, Apr 25, 14:00 - 16:00, Sal C

Degree of Sequentiality of Weighted Automata
Laure Daviaud, Ismaël Jecker, Pierre-Alain Reynier, and Didier Villevalois
(University of Warsaw, Poland; Université Libre de Bruxelles, Belgium; Aix-Marseille University, France)
Publisher's Version Article: etaps17fossacs-fossacsid25-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_13
Emptiness Under Isolation and the Value Problem for Hierarchical Probabilistic Automata
Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan
(University of Missouri, USA; University of Illinois at Chicago, USA; University of Illinois at Urbana-Champaign, USA)
Publisher's Version Article: etaps17fossacs-fossacsid108-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_14
Partial Derivatives for Context-Free Languages - From μ-Regular Expressions to Pushdown Automata
Peter Thiemann
(University of Freiburg, Germany)
Publisher's Version Article: etaps17fossacs-fossacsid4-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_15
Dynamic Complexity of the Dyck Reachability
Patricia Bouyer and Vincent Jugé
(CNRS, France; ENS Cachan, France; University of Paris-Saclay, France)
Publisher's Version Article: etaps17fossacs-fossacsid40-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_16

Proof Theory
Wed, Apr 26, 09:00 - 10:00, Sal C

Cyclic Arithmetic Is Equivalent to Peano Arithmetic
Alex Simpson
(University of Ljubljana, Slovenia)
Publisher's Version Best-Paper Award Nominee Article: etaps17fossacs-fossacsid60-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_17
Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System
Stefano Berardi and Makoto Tatsuta
(University of Turin, Italy; National Institute of Informatics, Japan)
Publisher's Version Best-Paper Award Nominee Article: etaps17fossacs-fossacsid22-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_18

Probability
Wed, Apr 26, 10:30 - 12:30, Sal C

On the Relationship Between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context
Gaoang Bian and Alessandro Abate
(Google, USA; University of Oxford, UK)
Publisher's Version Article: etaps17fossacs-fossacsid16-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_19
Computing Continuous-Time Markov Chains as Transformers of Unbounded Observables
Vincent Danos, Tobias Heindel, Ilias Garnier, and Jakob Grue Simonsen
(ENS, France; CNRS, France; University of Copenhagen, Denmark; University of Edinburgh, UK)
Publisher's Version Article: etaps17fossacs-fossacsid120-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_20
Pointless Learning
Florence Clerc, Vincent Danos, Fredrik Dahlqvist, and Ilias Garnier
(McGill University, Canada; ENS, France; CNRS, France; University College London, UK; University of Edinburgh, UK)
Publisher's Version Article: etaps17fossacs-fossacsid114-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_21
On Higher-Order Probabilistic Subrecursion
Flavien Breuvart, Ugo Dal Lago, and Agathe Herrou
(Inria, France; University of Bologna, Italy; ENS Lyon, France)
Publisher's Version Article: etaps17fossacs-fossacsid75-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_22

Concurrency
Thu, Apr 27, 10:30 - 12:30, Sal C

A Truly Concurrent Game Model of the Asynchronous π-Calculus
Ken Sakayori and Takeshi Tsukada
(University of Tokyo, Japan)
Publisher's Version Article: etaps17fossacs-fossacsid78-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_23
Local Model Checking in a Logic for True Concurrency
Paolo Baldan and Tommaso Padoan
(University of Padua, Italy)
Publisher's Version Article: etaps17fossacs-fossacsid89-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_24
The Paths to Choreography Extraction
Luís Cruz-Filipe, Kim S. Larsen, and Fabrizio Montesi
(University of Southern Denmark, Denmark)
Publisher's Version Article: etaps17fossacs-fossacsid26-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_25
On the Undecidability of Asynchronous Session Subtyping
Julien Lange and Nobuko Yoshida
(Imperial College London, UK)
Publisher's Version Article: etaps17fossacs-fossacsid20-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_26

Lambda Calculus and Constructive Proof
Wed, Apr 26, 16:30 - 18:00, Sal C

A Lambda-Free Higher-Order Recursive Path Order
Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand
(Inria, France; LORIA, France; Max Planck Institute for Informatics, Germany)
Publisher's Version Article: etaps17fossacs-fossacsid3-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_27
Automated Constructivization of Proofs
Frédéric Gilbert
(École des Ponts ParisTech, France; Inria, France; CEA LIST, France)
Publisher's Version Article: etaps17fossacs-fossacsid13-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_28

Semantics and Category Theory
Wed, Apr 26, 14:00 - 16:00, Sal C

A Light Modality for Recursion
Paula Severi
(University of Leicester, UK)
Publisher's Version Best-Paper Award Nominee Article: etaps17fossacs-fossacsid55-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_29
Unifying Guarded and Unguarded Iteration
Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Maciej Piróg
(University of Erlangen-Nuremberg, Germany; KU Leuven, Belgium)
Publisher's Version Article: etaps17fossacs-fossacsid70-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_30
Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type
Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus
(University of Nottingham, UK; University of Gothenburg, Sweden; Chalmers University of Technology, Sweden)
Publisher's Version Article: etaps17fossacs-fossacsid8-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_31
On the Semantics of Intensionality
G. A. Kavvos
(University of Oxford, UK)
Publisher's Version Article: etaps17fossacs-fossacsid81-p doi:http://dx.doi.org/10.1007/978-3-662-54458-7_32

POST

Information Flow
Mon, Apr 24, 10:30 - 12:30, Sal C

Timing-Sensitive Noninterference through Composition
Willard Rafnsson, Limin Jia, and Lujo Bauer
(MPI-SWS, Germany; Carnegie Mellon University, USA)
Publisher's Version Article: etaps17post-mainid18-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_1
Quantifying Vulnerability of Secret Generation Using Hyper-Distributions
Mário S. Alvim, Piotr Mardziel, and Michael W. Hicks
(Federal University of Minas Gerais, Brazil; Carnegie Mellon University, USA; University of Maryland at College Park, USA)
Publisher's Version Article: etaps17post-mainid17-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_2
A Principled Approach to Tracking Information Flow in the Presence of Libraries
Daniel Hedin, Alexander Sjösten, Frank Piessens, and Andrei Sabelfeld
(Mälardalen University, Sweden; Chalmers University of Technology, Sweden; KU Leuven, Belgium)
Publisher's Version Article: etaps17post-mainid43-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_3
Secure Multi-party Computation: Information Flow of Outputs and Game Theory
Patrick Ah-Fat and Michael Huth
(Imperial College London, UK)
Publisher's Version Article: etaps17post-mainid16-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_4

Security Protocols
Mon, Apr 24, 14:00 - 16:00, Sal C

Automated Verification of Dynamic Root of Trust Protocols
Sergiu Bursuc, Christian Johansen, and Shiwei Xu
(University of Bristol, UK; University of Oslo, Norway; Wuhan Digital and Engineering Institute, China)
Publisher's Version Article: etaps17post-mainid44-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_5
Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols
Jannik Dreier, Charles Duménil, Steve Kremer, and Ralf Sasse
(LORIA, France; CNRS, France; Inria, France; University of Lorraine, France; ETH Zurich, Switzerland)
Publisher's Version Article: etaps17post-mainid23-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_6
On Communication Models When Verifying Equivalence Properties
Kushal Babel, Vincent Cheval, and Steve Kremer
(IIT Bombay, India; Inria, France; LORIA, France; CNRS, France; University of Lorraine, France)
Publisher's Version Best-Paper Award Nominee Article: etaps17post-mainid32-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_7
A Survey of Attacks on Ethereum Smart Contracts (SoK)
Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli
(University of Cagliari, Italy)
Publisher's Version Article: etaps17post-mainid45-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_8

Security Policies
Tue, Apr 25, 10:30 - 12:30, Sal C

Security Analysis of Cache Replacement Policies
Pablo Cañones, Boris Köpf, and Jan Reineke
(IMDEA Software Institute, Spain; Saarland University, Germany)
Publisher's Version Best-Paper Award Nominee Article: etaps17post-mainid7-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_9
Model Checking Exact Cost for Attack Scenarios
Zaruhi Aslanyan and Flemming Nielson
(DTU, Denmark)
Publisher's Version Article: etaps17post-mainid15-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_10
Postulates for Revocation Schemes
Marcos Cramer and Giovanni Casini
(University of Luxembourg, Luxembourg)
Publisher's Version Article: etaps17post-mainid40-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_11
Defense in Depth Formulation and Usage in Dynamic Access Control
Ridha Khedri, Owain Jones, and Mohammed Alabbad
(McMaster University, Canada; CMC Microsystems, Canada)
Publisher's Version Article: etaps17post-mainid21-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_12

Information Leakage
Tue, Apr 25, 14:00 - 16:00, K3+K4

Compositional Synthesis of Leakage Resilient Programs
Arthur Blot, Masaki Yamamoto, and Tachio Terauchi
(ENS Lyon, France; Nagoya University, Japan; JAIST, Japan)
Publisher's Version Best-Paper Award Nominee Article: etaps17post-mainid20-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_13
Combining Differential Privacy and Mutual Information for Analyzing Leakages in Workflows
Martin Pettai and Peeter Laud
(Cybernetica, Estonia)
Publisher's Version Article: etaps17post-mainid8-p doi:http://dx.doi.org/10.1007/978-3-662-54455-6_14

TACAS

Validation, Synthesis, and Optimization for Cyber-Physical Systems (Invited Talk)
Kim G. Larsen
(Aalborg University, Denmark)
Mon, Apr 24, 09:00 - 10:00, Stora Salen, 6th Floor

Validation, Synthesis, and Optimization for Cyber-Physical Systems (Invited Talk)
Kim Guldstrand Larsen
(Aalborg University, Denmark)
Publisher's Version Article: etaps17tacas-tacasinv1-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_1

Verification Techniques 1
Mon, Apr 24, 10:30 - 12:30, Stora Salen, 6th Floor

An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP
Ocan Sankur and Jean-Pierre Talpin
(CNRS, France; IRISA, France; Inria, France)
Publisher's Version Article: etaps17tacas-tacasid24-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_2
Combining String Abstract Domains for JavaScript Analysis: An Evaluation
Roberto Amadini, Alexander Jordan, Graeme Gange, François Gauthier, Peter Schachte, Harald Søndergaard, Peter J. Stuckey, and Chenyi Zhang
(University of Melbourne, Australia; Oracle Labs, Australia; Oracle, Australia; University of Queensland, Australia)
Publisher's Version Article: etaps17tacas-tacasid62-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_3
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani
(Fondazione Bruno Kessler, Italy; University of Trento, Italy)
Publisher's Version Article: etaps17tacas-tacasid113-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_4
Bounded Quantifier Instantiation for Checking Inductive Invariants
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; University of Massachusetts at Amherst, USA)
Publisher's Version Article: etaps17tacas-tacasid45-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_5

Verification Techniques 2
Mon, Apr 24, 14:00 - 16:00, Stora Salen, 6th Floor

Proving Termination Through Conditional Termination
Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, and Albert Rubio
(Universitat de Vic, Spain; Microsoft Research, UK; Universitat Politècnica de Catalunya, Spain)
Publisher's Version Article: etaps17tacas-tacasid87-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_6
Efficient Certified Resolution Proof Checking
Luís Cruz-Filipe, Joao Marques-Silva, and Peter Schneider-Kamp
(University of Southern Denmark, Denmark; University of Lisbon, Portugal)
Publisher's Version Article: etaps17tacas-tacasid91-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_7
Precise Widening Operators for Proving Termination by Abstract Interpretation
Nathanaël Courant and Caterina Urban
(ENS, France; ETH Zurich, Switzerland)
Publisher's Version Article: etaps17tacas-tacasid120-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_8
Automatic Verification of Finite Precision Implementations of Linear Controllers
Junkil Park, Miroslav Pajic, Oleg Sokolsky, and Insup Lee
(University of Pennsylvania, USA; Duke University, USA)
Publisher's Version Article: etaps17tacas-tacasid162-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_9

Learning
Mon, Apr 24, 16:30 - 18:00, Sal B

Learning Symbolic Automata
Samuel Drews and Loris D'Antoni
(University of Wisconsin-Madison, USA)
Publisher's Version Best-Paper Award Nominee Article: etaps17tacas-tacasid3-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_10
ML for ML: Learning Cost Semantics by Experiment
Ankush Das and Jan Hoffmann
(Carnegie Mellon University, USA)
Publisher's Version Article: etaps17tacas-tacasid21-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_11
A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees
Yong Li, Yu-Fang Chen, Lijun Zhang, and Depeng Liu
(Institute of Software at Chinese Academy of Sciences, China; Academia Sinica, Taiwan)
Publisher's Version Article: etaps17tacas-tacasid102-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_12

Synthesis 1
Tue, Apr 25, 10:30 - 12:30, Stora Salen, 6th Floor

Hierarchical Network Formation Games
Orna Kupferman and Tami Tamir
(Hebrew University of Jerusalem, Israel; Interdisciplinary Center, Israel)
Publisher's Version Article: etaps17tacas-tacasid10-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_13
Synthesis of Recursive ADT Transformers from Reusable Templates
Jeevana Priya Inala, Nadia Polikarpova, Xiaokang Qiu, Benjamin S. Lerner, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA; Purdue University, USA; Northeastern University, USA)
Publisher's Version Article: etaps17tacas-tacasid30-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_14
Counterexample-Guided Model Synthesis
Mathias Preiner, Aina Niemetz, and Armin Biere
(JKU Linz, Austria)
Publisher's Version Article: etaps17tacas-tacasid42-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_15
Interpolation-Based GR(1) Assumptions Refinement
Davide G. Cavezza and Dalal Alrajeh
(Imperial College London, UK)
Publisher's Version Article: etaps17tacas-tacasid82-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_16

Synthesis 2
Tue, Apr 25, 14:00 - 16:00, Stora Salen, 6th Floor

Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation
ThanhVu Nguyen, Westley Weimer, Deepak Kapur, and Stephanie Forrest
(University of Nebraska-Lincoln, USA; University of Virginia, USA; University of New Mexico, USA)
Publisher's Version Article: etaps17tacas-tacasid105-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_17
Scaling Enumerative Program Synthesis via Divide and Conquer
Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa
(University of Pennsylvania, USA)
Publisher's Version Article: etaps17tacas-tacasid119-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_18
Towards Parallel Boolean Functional Synthesis
S. Akshay, Supratik Chakraborty, Ajith K. John, and Shetal Shah
(IIT Bombay, India; BARC, India)
Publisher's Version Article: etaps17tacas-tacasid214-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_19
Encodings of Bounded Synthesis
Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe, and Leander Tentrup
(Saarland University, Germany; University of California at Berkeley, USA)
Publisher's Version Article: etaps17tacas-tacasid215-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_20

Tools
Wed, Apr 26, 09:00 - 10:00, Stora Salen, 6th Floor

HQSpre - An Effective Preprocessor for QBF and DQBF
Ralf Wimmer, Sven Reimer, Paolo Marin, and Bernd Becker
(University of Freiburg, Germany)
Publisher's Version Article: etaps17tacas-tacasid52-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_21
RPP: Automatic Proof of Relational Properties by Self-composition
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, and Virgile Prevosto
(CEA LIST, France; CentraleSupélec, France)
Publisher's Version Article: etaps17tacas-tacasid150-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_22
autoCode4: Structural Controller Synthesis
Chih-Hong Cheng, Edward A. Lee, and Harald Ruess
(fortiss, Germany; University of California at Berkeley, USA)
Publisher's Version Article: etaps17tacas-tacasid13-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_23

Automata
Wed, Apr 26, 10:30 - 12:30, Stora Salen, 6th Floor

Lazy Automata Techniques for WS1S
Tomas Fiedor, Lukas Holik, Petr Janku, Ondrej Lengal, and Tomas Vojnar
(Brno University of Technology, Czech Republic)
Publisher's Version Article: etaps17tacas-tacasid44-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_24
From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
Javier Esparza, Jan Kretínský, Jean-François Raskin, and Salomon Sickert
(TU Munich, Germany; Université Libre de Bruxelles, Belgium)
Publisher's Version Article: etaps17tacas-tacasid69-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_25
Index Appearance Record for Transforming Rabin Automata into Parity Automata
Jan Kretínský, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger
(TU Munich, Germany)
Publisher's Version Article: etaps17tacas-tacasid167-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_26
Minimization of Visibly Pushdown Automata Using Partial Max-SAT
Matthias Heizmann, Christian Schilling, and Daniel Tischner
(University of Freiburg, Germany)
Publisher's Version Article: etaps17tacas-tacasid185-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_27

Concurrency and Bisimulation
Wed, Apr 26, 14:00 - 16:00, Stora Salen, 6th Floor

CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs
David Sanán, Yongwang Zhao, Zhe Hou, Fuyuan Zhang, Alwen Tiu, and Yang Liu
(Nanyang Technological University, Singapore; Beihang University, China; Australian National University, Australia)
Publisher's Version Article: etaps17tacas-tacasid25-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_28
Fair Termination for Parameterized Probabilistic Concurrent Systems
Ondrej Lengál, Anthony Widjaja Lin, Rupak Majumdar, and Phillip Rümmer
(Brno University of Technology, Czech Republic; Yale-NUS College, Singapore; MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version Article: etaps17tacas-tacasid96-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_29
Forward Bisimulations for Nondeterministic Symbolic Finite Automata
Loris D'Antoni and Margus Veanes
(University of Wisconsin-Madison, USA; Microsoft Research, USA)
Publisher's Version Article: etaps17tacas-tacasid2-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_30
Up-To Techniques for Weighted Systems
Filippo Bonchi, Barbara König, and Sebastian Küpper
(ENS Lyon, France; University of Duisburg-Essen, Germany)
Publisher's Version Article: etaps17tacas-tacasid130-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_31

Hybrid Systems
Wed, Apr 26, 16:30 - 18:00, Stora Salen, 6th Floor

Rigorous Simulation-Based Analysis of Linear Hybrid Systems
Stanley Bak and Parasara Sridhar Duggirala
(Air Force Research Lab, USA; University of Connecticut, USA)
Publisher's Version Article: etaps17tacas-tacasid227-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_32
HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata
Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA; Kansas State University, USA)
Publisher's Version Article: etaps17tacas-tacasid182-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_33
Counterexample-Guided Refinement of Template Polyhedra
Sergiy Bogomolov, Goran Frehse, Mirco Giacobbe, and Thomas A. Henzinger
(Australian National University, Australia; University of Grenoble, France; VERIMAG, France; IST Austria, Austria)
Publisher's Version Article: etaps17tacas-tacasid77-p doi:http://dx.doi.org/10.1007/978-3-662-54577-5_34

Security
Thu, Apr 27, 10:30 - 12:30, Stora Salen, 6th Floor

Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions
Valentin Wüstholz, Oswaldo Olivo, Marijn J. H. Heule, and Isil Dillig
(University of Texas at Austin, USA)
Publisher's Version Best-Paper Award Nominee Article: etaps17tacas-tacasid57-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_1
Discriminating Traces with Time
Saeid Tizpaz-Niari, Pavol Cerný, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Ashutosh Trivedi
(University of Colorado at Boulder, USA)
Publisher's Version Article: etaps17tacas-tacasid135-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_2
Directed Automated Memory Performance Testing
Sudipta Chattopadhyay
(Saarland University, Germany)
Publisher's Version Article: etaps17tacas-tacasid147-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_3
Context-Bounded Analysis for POWER
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo
(Uppsala University, Sweden; University of Paris Diderot, France)
Publisher's Version Best-Paper Award Nominee Article: etaps17tacas-tacasid177-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_4

Run-Time Verification and Logic
Thu, Apr 27, 16:30 - 18:00, Sal B

Rewriting-Based Runtime Verification of Alternation-Free HyperLTL
Noel Brett, Umair Siddique, and Borzoo Bonakdarpour
(McMaster University, Canada)
Publisher's Version Article: etaps17tacas-tacasid40-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_5
Almost Event-Rate Independent Monitoring of Metric Temporal Logic
David A. Basin, Bhargav Nagaraja Bhatt, and Dmitriy Traytel
(ETH Zurich, Switzerland)
Publisher's Version Article: etaps17tacas-tacasid76-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_6
Optimal Translation of LTL to Limit Deterministic Automata
Dileep Kini and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version Article: etaps17tacas-tacasid154-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_7

Quantitative Systems 1
Fri, Apr 28, 10:30 - 12:30, Stora Salen, 6th Floor

Sequential Convex Programming for the Efficient Verification of Parametric MDPs
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, and Ufuk Topcu
(University of Texas at Austin, USA; RWTH Aachen University, Germany)
Publisher's Version Article: etaps17tacas-tacasid169-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_8
JANI: Quantitative Model and Tool Interaction
Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges, and Andrea Turrini
(Universidad Nacional de Córdoba, Argentina; RWTH Aachen University, Germany; Institute of Software at Chinese Academy of Sciences, China; University of Twente, Netherlands)
Publisher's Version Article: etaps17tacas-tacasid39-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_9
Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults
Guy Avni, Shubham Goel, Thomas A. Henzinger, and Guillermo Rodríguez-Navas
(IST Austria, Austria; IIT Bombay, India; Mälardalen University, Sweden)
Publisher's Version Article: etaps17tacas-tacasid50-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_10
Long-Run Rewards for Markov Automata
Yuliya Butkova, Ralf Wimmer, and Holger Hermanns
(Saarland University, Germany; University of Freiburg, Germany)
Publisher's Version Article: etaps17tacas-tacasid209-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_11

SAT and SMT
Fri, Apr 28, 14:00 - 16:00, Stora Salen, 6th Floor

HiFrog: SMT-based Function Summarization for Software Verification
Leonardo Alt, Sepideh Asadi, Hana Chockler, Karine Even Mendoza, Grigory Fedyukovich, Antti E. J. Hyvärinen, and Natasha Sharygina
(University of Lugano, Switzerland; King's College London, UK; University of Washington, USA)
Publisher's Version Article: etaps17tacas-tacasid56-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_12
Congruence Closure with Free Variables
Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds
(LORIA, France; Inria, France; University of Lorraine, France; University of Iowa, USA)
Publisher's Version Article: etaps17tacas-tacasid72-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_13
On Optimization Modulo Theories, MaxSMT and Sorting Networks
Roberto Sebastiani and Patrick Trentin
(University of Trento, Italy)
Publisher's Version Article: etaps17tacas-tacasid116-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_14
The Automatic Detection of Token Structures and Invariants Using SAT Checking
Pedro R. G. Antonino, Thomas Gibson-Robinson, and A. W. Roscoe
(Federal University of Pernambuco, Brazil; University of Oxford, UK)
Publisher's Version Article: etaps17tacas-tacasid123-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_15

Quantitative Systems 2
Fri, Apr 28, 16:30 - 18:00, Stora Salen, 6th Floor

Maximizing the Conditional Expected Reward for Reaching the Goal
Christel Baier, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich
(TU Dresden, Germany)
Publisher's Version Article: etaps17tacas-tacasid163-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_16
ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans
Anna Lukina, Lukas Esterle, Christian Hirsch, Ezio Bartocci, Junxing Yang, Ashish Tiwari, Scott A. Smolka, and Radu Grosu
(Vienna University of Technology, Austria; Stony Brook University, USA; SRI International, USA)
Publisher's Version Article: etaps17tacas-tacasid101-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_17
FlyFast: A Mean Field Model Checker
Diego Latella, Michele Loreti, and Mieke Massink
(ISTI-CNR, Italy; University of Florence, Italy)
Publisher's Version Article: etaps17tacas-tacasid65-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_18
ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations
Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin
(Microsoft Research, UK; IMT School for Advanced Studies Lucca, Italy)
Publisher's Version Article: etaps17tacas-tacasid144-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_19

Competition on Software Verification (SV-COMP)
Thu, Apr 27, 14:00 - 16:00, Stora Salen, 6th Floor

Software Verification with Validation of Results (Report on SV-COMP 2017)
Dirk Beyer
(LMU Munich, Germany)
Publisher's Version Article: etaps17tacas-tacassvcompid000-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_20
AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (Competition Contribution)
Jera Hensel, Frank Emrich, Florian Frohn, Thomas Ströder, and Jürgen Giesl
(RWTH Aachen University, Germany)
Publisher's Version Article: etaps17tacas-tacassvcompid14-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_21
CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution)
Pavel Andrianov, Karlheinz Friedberger, Mikhail U. Mandrykin, Vadim S. Mutilin, and Anton Volkov
(ISP RAS, Russia; University of Passau, Germany)
Publisher's Version Article: etaps17tacas-tacassvcompid21-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_22
DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs (Competition Contribution)
Williame Rocha, Herbert Rocha, Hussama Ismail, Lucas C. Cordeiro, and Bernd Fischer
(Federal University of Amazonas, Brazil; Federal University of Roraima, Brazil; University of Oxford, UK; Stellenbosch University, South Africa)
Publisher's Version Article: etaps17tacas-tacassvcompid26-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_23
Forester: From Heap Shapes to Automata Predicates (Competition Contribution)
Lukás Holík, Martin Hruska, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, and Tomás Vojnar
(Brno University of Technology, Czech Republic)
Publisher's Version Article: etaps17tacas-tacassvcompid16-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_24
HipTNT+: A Termination and Non-termination Analyzer by Second-Order Abduction (Competition Contribution)
Ton Chanh Le, Quang-Trung Ta, and Wei-Ngan Chin
(National University of Singapore, Singapore)
Publisher's Version Article: etaps17tacas-tacassvcompid12-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_25
Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation (Competition Contribution)
Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato
(University of Southampton, UK; Stellenbosch University, South Africa; University of Salerno, Italy)
Publisher's Version Article: etaps17tacas-tacassvcompid23-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_26
Skink: Static Analysis of Programs in LLVM Intermediate Representation (Competition Contribution)
Franck Cassez, Anthony M. Sloane, Matthew Roberts, Matthew Pigram, Pongsak Suvanpong, and Pablo González de Aledo Marugán
(Macquarie University, Australia; University of Cantabria, Spain)
Publisher's Version Article: etaps17tacas-tacassvcompid13-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_27
Symbiotic 4: Beyond Reachability (Competition Contribution)
Marek Chalupa, Martina Vitovská, Martin Jonáš, Jiri Slaby, and Jan Strejcek
(Masaryk University, Czech Republic)
Publisher's Version Article: etaps17tacas-tacassvcompid29-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_28
Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)
Jan Mrázek, Martin Jonáš, Vladimír Štill, Henrich Lauko, and Jiří Barnat
(Masaryk University, Czech Republic)
Publisher's Version Article: etaps17tacas-tacassvcompid28-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_29
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata (Competition Contribution)
Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus, Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling, Frank Schüssele, and Andreas Podelski
(University of Freiburg, Germany)
Publisher's Version Article: etaps17tacas-tacassvcompid33-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_30
Ultimate Taipan: Trace Abstraction and Abstract Interpretation (Competition Contribution)
Marius Greitschus, Daniel Dietsch, Matthias Heizmann, Alexander Nutz, Claus Schätzle, Christian Schilling, Frank Schüssele, and Andreas Podelski
(University of Freiburg, Germany)
Publisher's Version Article: etaps17tacas-tacassvcompid31-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_31
VeriAbs: Verification by Abstraction (Competition Contribution)
Bharti Chimdyalwar, Priyanka Darke, Avriti Chauhan, Punit Shah, Shrawan Kumar, and R. Venkatesh
(Tata Consultancy Services, India)
Publisher's Version Article: etaps17tacas-tacassvcompid17-p doi:http://dx.doi.org/10.1007/978-3-662-54580-5_32

proc time: 0.19