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

ETAPS 2017 Wednesday

Wednesday, April 26, 2017

Graph Rewriting (ESOP)
09:00 – 10:00, Sal B
Session chair: Sam Staton
 		Learning and Inference (FASE)
09:00 – 10:00, K3+K4
Session chair: Reiko Heckel
 		Proof Theory (FOSSACS)
09:00 – 10:00, Sal C
Session chair: Andrzej Murawski
 		Tools (TACAS)
09:00 – 10:00, Stora Salen, 6th Floor
Dave Parker
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
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 Preprint Info
Cyclic Arithmetic Is Equivalent to Peano Arithmetic
Alex Simpson
(University of Ljubljana, Slovenia)
Best-Paper Award Nominee
Publisher's Version
HQSpre - An Effective Preprocessor for QBF and DQBF
Ralf Wimmer, Sven Reimer, Paolo Marin, and Bernd Becker
(University of Freiburg, Germany)
Publisher's Version Preprint
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 Preprint
Bordeaux: A Tool for Thinking Outside the Box
Vajih Montaghami and Derek Rayside
(University of Waterloo, Canada)
Publisher's Version
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)
Best-Paper Award Nominee
Publisher's Version
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 Preprint
     
autoCode4: Structural Controller Synthesis
Chih-Hong Cheng, Edward A. Lee, and Harald Ruess
(fortiss, Germany; University of California at Berkeley, USA)
Publisher's Version Video
Coffee Break
10:00 – 10:30, 3rd and 6th Floor
Concurrency (ESOP)
10:30 – 12:30, Sal B
Session chair: Nobuko Yoshida
 		Test Selection (FASE)
10:30 – 12:30, K3+K4
Session chair: Andy Schürr
 		Probability (FOSSACS)
10:30 – 12:30, Sal C
Session chair: Christel Baier
 		Automata (TACAS)
10:30 – 12:30, Stora Salen, 6th Floor
Session chair: Radu Grosu
Abstract Specifications for Concurrent Maps
Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik, and Philippa Gardner
(Imperial College London, UK)
Publisher's Version Preprint Info
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 Preprint
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 Preprint
Lazy Automata Techniques for WS1S
Tomas Fiedor, Lukás Holík, Petr Janku, Ondrej Lengál, and Tomás Vojnar
(Brno University of Technology, Czech Republic)
Publisher's Version Preprint Info
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 Preprint Video Info
Selective Bisection Debugging
Ripon Saha and Milos Gligoric
(Fujitsu Labs, USA; University of Texas at Austin, USA)
Publisher's Version
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 Preprint
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 Preprint
Observed Communication Semantics for Classical Processes
Robert Atkey
(University of Strathclyde, UK)
Publisher's Version Preprint
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 Preprint Info
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 Preprint
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 Preprint
Tackling Real-Life Relaxed Concurrency with FSL++
Marko Doko and Viktor Vafeiadis
(MPI-SWS, Germany)
Publisher's Version Preprint Info
 
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 Preprint
Minimization of Visibly Pushdown Automata Using Partial Max-SAT
Matthias Heizmann, Christian Schilling, and Daniel Tischner
(University of Freiburg, Germany)
Publisher's Version Preprint

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

ETAPS Association General Assembly
13:00 - 14:00, Sal C
Language Design (ESOP)
14:00 – 16:00, Sal B
Session chair: Sam Staton
 		Semantics and Category Theory (FOSSACS)
14:00 – 16:00, Sal C
Session chair: Alex Simpson
 		Concurrency and Bisimulation (TACAS)
14:00 – 16:00, Stora Salen, 6th Floor
Session chair: Gerald Luettgen
APLicative Programming with Naperian Functors
Jeremy Gibbons
(University of Oxford, UK)
Publisher's Version Preprint Info
A Light Modality for Recursion
Paula Severi
(University of Leicester, UK)
Best-Paper Award Nominee
Publisher's Version Preprint
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 Preprint
Disjoint Polymorphism
João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi
(University of Hong Kong, China)
Publisher's Version
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 Preprint
Fair Termination for Parameterized Probabilistic Concurrent Systems
Ondrej Lengál, Anthony Widjaja Lin, Rupak Majumdar, and Philipp Rümmer
(Brno University of Technology, Czech Republic; Yale-NUS College, Singapore; MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version
Extensible Datasort Refinements
Joshua Dunfield
(University of British Columbia, Canada)
Publisher's Version
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
Forward Bisimulations for Nondeterministic Symbolic Finite Automata
Loris D'Antoni and Margus Veanes
(University of Wisconsin-Madison, USA; Microsoft Research, USA)
Publisher's Version Preprint
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
On the Semantics of Intensionality
G. A. Kavvos
(University of Oxford, UK)
Publisher's Version Preprint
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 Preprint
Coffee Break
16:00 – 16:30, 3rd and 6th Floor
Verification (ESOP)
16:30 – 18:00, Sal B
Session chair: Robert Atkey

Lambda Calculus and Constructive Proof (FOSSACS)
16:30 – 18:00, Sal C
Session chair: Simona Ronchi Della Rocca

 Hybrid Systems (TACAS)
16:30 – 18:00, Stora Salen, 6th Floor
Session chair: Borzoo Bonakdarpour
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 Preprint
A Lambda-Free Higher-Order Recursive Path Order
, Uwe Waldmann, and Daniel Wand
(Inria, France; LORIA, France; Max Planck Institute for Informatics, Germany)
Publisher's Version Preprint
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 Preprint Video Info
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
Automated Constructivization of Proofs
Frédéric Gilbert
(École des Ponts ParisTech, France; Inria, France; CEA LIST, France)
Publisher's Version
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
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
Coherence Spaces and Uniform Continuity
Kei Matsumoto
(Kyoto University, Japan)
Publisher's Version
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 Preprint
Conference Banquet
19:00 – 22:00, Uppsala Castle