ETAPS 2017 Friday

Friday, April 28, 2017

Plenary 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 Arthur Charguéraud and François Pottier (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 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 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 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 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 Zheng Cheng and Massimo Tisi (AtlanMod, France) Best-Paper Award Nominee Publisher's Version Preprint Video Info	Long-Run Rewards for Markov Automata Yuliya Butkova, Ralf Wimmer, and Holger Hermanns (Saarland University, Germany; University of Freiburg, Germany) Publisher's Version Preprint Info

Lunch 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	SAT and SMT (TACAS) 14:00 – 16:00, Stora Salen, 6th Floor Session chair: Natasha Sharygina
Context-Free Session Type Inference Luca Padovani (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 Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds (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 Maurice H. ter Beek, Erik P. de Vink, and Tim A. C. Willemse (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 Aleksandar S. Dimovski and Andrzej Wąsowski (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 Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin (Microsoft Research, UK; IMT School for Advanced Studies Lucca, Italy) Publisher's Version Preprint