ETAPS 2017: 22-29 April 2017, Uppsala, Sweden

ETAPS 2017 Friday

Friday, April 28, 2017

09:00 – 10:00, Stora Salen, 6th Floor
Invited Talk: Fundamental Algorithmic Problems and Challenges in Dynamical and Cyber-Physical Systems
Joel Ouaknine
(University of Oxford, UK)

Coffee Break
10:00 – 10:30, 3rd and 6th Floor

Separation Logic (ESOP)
10:30 – 12:30, Sal B
Session chair: Hongseok Yang
Model Transformations (FASE)
10:30 – 12:30, Sal C
Session chair: Fernando Orejas
Quantitative Systems 1 (TACAS)
10:30 – 12:30, Stora Salen, 6th Floor
Session chair: Christel Baier
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 Preprint
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 Preprint
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 Preprint
Temporary Read-Only Permissions for Separation Logic
(Inria, France)
Publisher's Version Preprint Info
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 Preprint
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
The Essence of Higher-Order Concurrent Separation Logic
(Delft University of Technology, Netherlands; MPI-SWS, Germany; Aarhus University, Denmark)
Publisher's Version Preprint
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 Info
Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults
(IST Austria, Austria; IIT Bombay, India; Mälardalen University, Sweden)
Publisher's Version Preprint Info
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 Preprint
A Deductive Approach for Fault Localization in ATL Model Transformations
(AtlanMod, France)
Best-Paper Award Nominee
Publisher's Version Preprint Video Info
Long-Run Rewards for Markov Automata
(Saarland University, Germany; University of Freiburg, Germany)
Publisher's Version Preprint Info

12:30 – 14:00, Sal D, Street Level

Session Types (ESOP)
14:00 – 16:00, Sal B
Session chair: Nobuko Yoshida
Configuration and Synthesis (FASE)
14:00 – 16:00, Sal C
Session chair: Marieke Huisman
14:00 – 16:00, Stora Salen, 6th Floor
Session chair: Natasha Sharygina
Context-Free Session Type Inference
(University of Turin, Italy)
Best-Paper Award Nominee
Publisher's Version Preprint Info
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 Info
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 Info
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
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
Congruence Closure with Free Variables
(LORIA, France; Inria, France; University of Lorraine, France; University of Iowa, USA)
Publisher's Version Preprint
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
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 Preprint Info
On Optimization Modulo Theories, MaxSMT and Sorting Networks
Roberto Sebastiani and Patrick Trentin
(University of Trento, Italy)
Publisher's Version Preprint Info
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 Preprint
Slicing from Formal Sematics: Chisel
Adrián Riesco, Irina Mariuca Asavoae, and Mihail Asavoae
(Complutense University of Madrid, Spain; Inria, France)
Publisher's Version Preprint Info
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
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 Preprint Video Info

Coffee Break
16:00 – 16:30, 3rd and 6th Floor

Type Theory (ESOP)
16:30 – 18:00, Sal B
Session chair: Hongseok Yang
Software Product Lines (FASE)
16:30 – 18:00, Sal C
Session chair: Julia Rubin
Quantitative Systems 2 (TACAS)
16:30 – 18:00, Stora Salen, 6th Floor
Session chair: Holger Hermanns
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
Family-Based Model Checking with mCRL2
(ISTI-CNR, Italy; Eindhoven University of Technology, Netherlands)
Publisher's Version
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 Preprint
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
Variability-Specific Abstraction Refinement for Family-Based Model Checking
(IT University of Copenhagen, Denmark)
Publisher's Version Preprint
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 Preprint
Programs Using Syntax with First-Class Binders
Francisco Ferreira and Brigitte Pientka
(McGill University, Canada)
Publisher's Version
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
FlyFast: A Mean Field Model Checker
Diego Latella, Michele Loreti, and Mieke Massink
(ISTI-CNR, Italy; University of Florence, Italy)
Publisher's Version
ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations
(Microsoft Research, UK; IMT School for Advanced Studies Lucca, Italy)
Publisher's Version Preprint