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
(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
(Singapore University of Technology and Design, Singapore; University of Luxembourg, Luxembourg)
Publisher's Version Preprint  Info |
Cyclic Arithmetic Is Equivalent to Peano Arithmetic
(University of Ljubljana, Slovenia)
Best-Paper Award Nominee Publisher's Version |
HQSpre - An Effective Preprocessor for QBF and DQBF
(University of Freiburg, Germany)
Publisher's Version Preprint  |
|
Incremental Update for Graph Rewriting
(Harvard Medical School, USA; University of Paris Diderot, France; CNRS, France; amp, France)
Publisher's Version Preprint  |
Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System
(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
(CEA LIST, France; CentraleSupélec, France)
Publisher's Version Preprint  |
|
|
autoCode4: Structural Controller Synthesis
(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
(Imperial College London, UK)
Publisher's Version Preprint Info    |
Bucketing Failing Tests via Symbolic Analysis
(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
(Google, USA; University of Oxford, UK)
Publisher's Version Preprint |
Lazy Automata Techniques for WS1S
(Brno University of Technology, Czech Republic)
Publisher's Version Preprint Info   |
|
Caper - Automatic Verification for Fine-Grained Concurrency
(Aarhus University, Denmark; Imperial College London, UK)
Publisher's Version Preprint Video Info  |
Selective Bisection Debugging
(Fujitsu Labs, USA; University of Texas at Austin, USA)
Publisher's Version |
Computing Continuous-Time Markov Chains as Transformers of Unbounded Observables
(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
(TU Munich, Germany; Université Libre de Bruxelles, Belgium)
Publisher's Version Preprint |
|
Observed Communication Semantics for Classical Processes
(University of Strathclyde, UK)
Publisher's Version Preprint |
On the Effectiveness of Bug Predictors with Procedural Systems: A Quantitative Study
(Federal University of Rio Grande do Sul, Brazil)
Publisher's Version Preprint Info    |
Pointless Learning
(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
(TU Munich, Germany)
Publisher's Version Preprint |
|
Tackling Real-Life Relaxed Concurrency with FSL++
(MPI-SWS, Germany)
Publisher's Version Preprint Info   |
On Higher-Order Probabilistic Subrecursion
(Inria, France; University of Bologna, Italy; ENS Lyon, France)
Publisher's Version Preprint   |
Minimization of Visibly Pushdown Automata Using Partial Max-SAT
(University of Freiburg, Germany)
Publisher's Version Preprint  |
|
|
Lunch ETAPS Association General Assembly |
|||
| 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
(University of Oxford, UK)
Publisher's Version Preprint Info  |
A Light Modality for Recursion
(University of Leicester, UK)
Best-Paper Award Nominee Publisher's Version Preprint  |
CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs
(Nanyang Technological University, Singapore; Beihang University, China; Australian National University, Australia)
Publisher's Version Preprint  |
|
|
Unifying Guarded and Unguarded Iteration
(University of Erlangen-Nuremberg, Germany; KU Leuven, Belgium)
Publisher's Version Preprint   |
Fair Termination for Parameterized Probabilistic Concurrent Systems
(Brno University of Technology, Czech Republic; Yale-NUS College, Singapore; MPI-SWS, Germany; Uppsala University, Sweden)
Publisher's Version |
||
|
Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type
(University of Nottingham, UK; University of Gothenburg, Sweden; Chalmers University of Technology, Sweden)
Publisher's Version  |
Forward Bisimulations for Nondeterministic Symbolic Finite Automata
(University of Wisconsin-Madison, USA; Microsoft Research, USA)
Publisher's Version Preprint  |
||
|
The Essence of Functional Programming on Semantic Data
(University of Koblenz-Landau, Germany; University of Southampton, UK)
Publisher's Version    |
Up-To Techniques for Weighted Systems
(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) |
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
(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
(Inria, France; LORIA, France; Max Planck Institute for Informatics, Germany)
Publisher's Version Preprint |
Rigorous Simulation-Based Analysis of Linear Hybrid Systems
(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
(Imperial College London, UK; Microsoft Research, USA)
Publisher's Version |
Automated Constructivization of Proofs
(É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
(University of Illinois at Urbana-Champaign, USA; Kansas State University, USA)
Publisher's Version |
|
|
Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency
(University of Paris Diderot, France; Nokia Bell Labs, USA; Koç University, Turkey)
Publisher's Version |
Counterexample-Guided Refinement of Template Polyhedra
(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 |
|||