ETAPS 2017
2017 European Joint Conferences on Theory and Practice of Software (ETAPS)

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

Phone Layout
No Pictures
Monday, April 24, 2017
Registration (Business)
08:00 – 08:30, Street Level
Opening
08:30 – 09:00, Stora Salen, 6th Floor
Opening
Joost-Pieter Katoen and Parosh Aziz Abdulla
(RWTH Aachen University, Germany; Uppsala University, Sweden)
Validation, Synthesis, and Optimization for Cyber-Physical Systems (Invited Talk)
09:00 – 10:00, Stora Salen, 6th Floor
Validation, Synthesis, and Optimization for Cyber-Physical Systems (Invited Talk)
Publisher's Version
Coffee Break
10:00 – 10:30, 3rd and 6th Floor
Coherence Spaces and Higher-Order Computation (FOSSACS)
10:30 – 12:30, Sal B
Information Flow (POST)
10:30 – 12:30, Sal C
Verification Techniques 1 (TACAS)
10:30 – 12:30, Stora Salen, 6th Floor
Coherence Spaces and Uniform Continuity
Publisher's Version
Timing-Sensitive Noninterference through Composition
Publisher's Version Preprint Info
An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP
Publisher's Version Preprint Info
The Free Exponential Modality of Probabilistic Coherence Spaces
Publisher's Version
Quantifying Vulnerability of Secret Generation Using Hyper-Distributions
Publisher's Version Preprint Info
Combining String Abstract Domains for JavaScript Analysis: An Evaluation
Publisher's Version Preprint
From Qualitative to Quantitative Semantics - By Change of Base
Publisher's Version
A Principled Approach to Tracking Information Flow in the Presence of Libraries
Publisher's Version Preprint
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
Publisher's Version Preprint Info
Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence
Publisher's Version
Secure Multi-party Computation: Information Flow of Outputs and Game Theory
Publisher's Version
Bounded Quantifier Instantiation for Checking Inductive Invariants
Publisher's Version Preprint
Lunch
12:30 – 14:00, Sal D, Street Level
Algebra and Coalgebra (FOSSACS)
14:00 – 16:00, Sal B
Security Protocols (POST)
14:00 – 16:00, Sal C
Verification Techniques 2 (TACAS)
14:00 – 16:00, Stora Salen, 6th Floor
Algebra, Coalgebra, and Minimization in Polynomial Differential Equations
Best-Paper Award Nominee
Publisher's Version Preprint Info
Automated Verification of Dynamic Root of Trust Protocols
Publisher's Version Preprint
Proving Termination Through Conditional Termination
Publisher's Version Preprint Info
Equational Theories of Abnormal Termination Based on Kleene Algebra
Publisher's Version
Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols
Publisher's Version Preprint Info
Efficient Certified Resolution Proof Checking
Publisher's Version Preprint
Companions, Codensity and Causality
Publisher's Version Preprint
On Communication Models When Verifying Equivalence Properties
Best-Paper Award Nominee
Publisher's Version Preprint Info
Precise Widening Operators for Proving Termination by Abstract Interpretation
Publisher's Version Preprint
Nominal Automata with Name Binding
Publisher's Version Preprint
A Survey of Attacks on Ethereum Smart Contracts (SoK)
Publisher's Version Preprint
Automatic Verification of Finite Precision Implementations of Linear Controllers
Publisher's Version Preprint
Coffee Break
16:00 – 16:30, 3rd and 6th Floor
Secure Composition of Security Protocols (Tutorial 1)
16:30 – 18:00, Stora Salen, 6th Floor
Learning (TACAS)
16:30 – 18:00, Sal B
Secure Composition of Security Protocols (Tutorial 1)
Veronique Cortier
(CNRS, France)
Learning Symbolic Automata
Best-Paper Award Nominee
Publisher's Version Preprint
ML for ML: Learning Cost Semantics by Experiment
Publisher's Version Preprint Info
A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees
Publisher's Version Preprint
Reception
18:30 – 22:00, 6th Floor
Tuesday, April 25, 2017
The Facebook Infer Static Analyser (Invited Talk)
09:00 – 10:00, Stora Salen, 6th Floor
The Facebook Infer Static Analyser (Invited Talk)
Dino Distefano
(Facebook, UK)
Coffee Break
10:00 – 10:30, 3rd and 6th Floor
Games and Automata (FOSSACS)
10:30 – 12:30, Sal B
Security Policies (POST)
10:30 – 12:30, Sal C
Synthesis 1 (TACAS)
10:30 – 12:30, Stora Salen, 6th Floor
On the Existence of Weak Subgame Perfect Equilibria
Publisher's Version Preprint
Security Analysis of Cache Replacement Policies
Best-Paper Award Nominee
Publisher's Version Preprint
Hierarchical Network Formation Games
Publisher's Version Preprint
Optimal Reachability in Divergent Weighted Timed Games
Publisher's Version
Model Checking Exact Cost for Attack Scenarios
Publisher's Version
Synthesis of Recursive ADT Transformers from Reusable Templates
Publisher's Version Preprint
Bounding Average-Energy Games
Publisher's Version Preprint
Postulates for Revocation Schemes
Publisher's Version Preprint Info
Counterexample-Guided Model Synthesis
Publisher's Version Preprint Info
Logics of Repeating Values on Data Trees and Branching Counter Systems
Publisher's Version Preprint
Defense in Depth Formulation and Usage in Dynamic Access Control
Publisher's Version Preprint
Interpolation-Based GR(1) Assumptions Refinement
Publisher's Version Preprint Info
Lunch
12:30 – 14:00, Sal D, Street Level
Probabilistic Programming (ESOP)
14:00 – 16:00, Sal B
Automata, Logic, and Formal Languages (FOSSACS)
14:00 – 16:00, Sal C
Information Leakage (POST)
14:00 – 16:00, K3+K4
Synthesis 2 (TACAS)
14:00 – 16:00, Stora Salen, 6th Floor
Commutative Semantics for Probabilistic Programming
Best-Paper Award Nominee
Publisher's Version Preprint
Degree of Sequentiality of Weighted Automata
Publisher's Version
Compositional Synthesis of Leakage Resilient Programs
Best-Paper Award Nominee
Publisher's Version
Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation
Publisher's Version Preprint
Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring
Best-Paper Award Nominee
Publisher's Version
Emptiness Under Isolation and the Value Problem for Hierarchical Probabilistic Automata
Publisher's Version
Combining Differential Privacy and Mutual Information for Analyzing Leakages in Workflows
Publisher's Version
Scaling Enumerative Program Synthesis via Divide and Conquer
Publisher's Version
Metric Reasoning About λ-Terms: The General Case
Publisher's Version
Partial Derivatives for Context-Free Languages - From μ-Regular Expressions to Pushdown Automata
Publisher's Version
Towards Parallel Boolean Functional Synthesis
Publisher's Version Preprint
Probabilistic Termination by Monadic Affine Sized Typing
Publisher's Version Preprint Info
Dynamic Complexity of the Dyck Reachability
Publisher's Version
Encodings of Bounded Synthesis
Publisher's Version
Coffee Break
16:00 – 16:30, 3rd and 6th Floor
Issues in Ethical Data Management (Public Lecture)
16:30 – 18:00, Stora Salen, 6th Floor
Issues in Ethical Data Management (Public Lecture)
Serge Abiteboul
(INRIA, France)
ETAPS SC Meeting and Dinner (Business)
18:30 – 23:00, Hotel Villa Anna, Odinslund 3
Wednesday, April 26, 2017
Graph Rewriting (ESOP)
09:00 – 10:00, Sal B
Learning and Inference (FASE)
09:00 – 10:00, K3+K4
Proof Theory (FOSSACS)
09:00 – 10:00, Sal C
Tools (TACAS)
09:00 – 10:00, Stora Salen, 6th Floor
Confluence of Graph Rewriting with Interfaces
Publisher's Version
Should We Learn Probabilistic Models for Model Checking? A New Approach and An Empirical Study
Publisher's Version Preprint Info
Cyclic Arithmetic Is Equivalent to Peano Arithmetic
Best-Paper Award Nominee
Publisher's Version
HQSpre - An Effective Preprocessor for QBF and DQBF
Publisher's Version Preprint
Incremental Update for Graph Rewriting
Publisher's Version Preprint
Bordeaux: A Tool for Thinking Outside the Box
Publisher's Version
Classical System of Martin-Löf's Inductive Definitions Is Not Equivalent to Cyclic Proof System
Best-Paper Award Nominee
Publisher's Version
RPP: Automatic Proof of Relational Properties by Self-composition
Publisher's Version Preprint
autoCode4: Structural Controller Synthesis
Publisher's Version Video
Coffee Break
10:00 – 10:30, 3rd and 6th Floor
Concurrency (ESOP)
10:30 – 12:30, Sal B
Test Selection (FASE)
10:30 – 12:30, K3+K4
Probability (FOSSACS)
10:30 – 12:30, Sal C
Automata (TACAS)
10:30 – 12:30, Stora Salen, 6th Floor
Abstract Specifications for Concurrent Maps
Publisher's Version Preprint Info
Bucketing Failing Tests via Symbolic Analysis
Publisher's Version Preprint
On the Relationship Between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context
Publisher's Version Preprint
Lazy Automata Techniques for WS1S
Publisher's Version Preprint Info
Caper - Automatic Verification for Fine-Grained Concurrency
Publisher's Version Preprint Video Info
Selective Bisection Debugging
Publisher's Version
Computing Continuous-Time Markov Chains as Transformers of Unbounded Observables
Publisher's Version Preprint
From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
Publisher's Version Preprint
Observed Communication Semantics for Classical Processes
Publisher's Version Preprint
On the Effectiveness of Bug Predictors with Procedural Systems: A Quantitative Study
Publisher's Version Preprint Info
Pointless Learning
Publisher's Version Preprint
Index Appearance Record for Transforming Rabin Automata into Parity Automata
Publisher's Version Preprint
Tackling Real-Life Relaxed Concurrency with FSL++
Publisher's Version Preprint Info
On Higher-Order Probabilistic Subrecursion
Publisher's Version Preprint
Minimization of Visibly Pushdown Automata Using Partial Max-SAT
Publisher's Version Preprint
Lunch
12:30 – 14:00, Sal D, Street Level
Language Design (ESOP)
14:00 – 16:00, Sal B
Semantics and Category Theory (FOSSACS)
14:00 – 16:00, Sal C
Concurrency and Bisimulation (TACAS)
14:00 – 16:00, Stora Salen, 6th Floor
APLicative Programming with Naperian Functors
Publisher's Version Preprint Info
A Light Modality for Recursion
Best-Paper Award Nominee
Publisher's Version Preprint
CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs
Publisher's Version Preprint
Disjoint Polymorphism
Publisher's Version
Unifying Guarded and Unguarded Iteration
Publisher's Version Preprint
Fair Termination for Parameterized Probabilistic Concurrent Systems
Publisher's Version
Extensible Datasort Refinements
Publisher's Version Preprint
Partiality, Revisited - The Partiality Monad as a Quotient Inductive-Inductive Type
Publisher's Version
Forward Bisimulations for Nondeterministic Symbolic Finite Automata
Publisher's Version Preprint
The Essence of Functional Programming on Semantic Data
Publisher's Version
On the Semantics of Intensionality
Publisher's Version Preprint
Up-To Techniques for Weighted Systems
Publisher's Version Preprint
Coffee Break
16:00 – 16:30, 3rd and 6th Floor
Verification (ESOP)
16:30 – 18:00, Sal B
Lambda Calculus and Constructive Proof (FOSSACS)
16:30 – 18:00, Sal C
Hybrid Systems (TACAS)
16:30 – 18:00, Stora Salen, 6th Floor
Is Your Software on Dope? Formal Analysis of Surreptitiously "enhanced" Programs
Publisher's Version Preprint
A Lambda-Free Higher-Order Recursive Path Order
Publisher's Version Preprint
Rigorous Simulation-Based Analysis of Linear Hybrid Systems
Publisher's Version Preprint Video Info
Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
Publisher's Version
Automated Constructivization of Proofs
Publisher's Version
HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata
Publisher's Version
Verifying Robustness of Event-Driven Asynchronous Programs Against Concurrency
Publisher's Version
Counterexample-Guided Refinement of Template Polyhedra
Publisher's Version Preprint
Conference Banquet
19:00 – 22:00, Uppsala Castle
Thursday, April 27, 2017
Natural Language is a Programming Language (Invited Talk)
09:00 – 10:00, Stora Salen, 6th Floor
Natural Language is a Programming Language (Invited Talk)
Michael Ernst
(University of Washington, USA)
Coffee Break
10:00 – 10:30, 3rd and 6th Floor
Automated Verification (ESOP)
10:30 – 12:30, Sal B
Program and System Analysis (FASE)
10:30 – 12:30, K3+K4
Concurrency (FOSSACS)
10:30 – 12:30, Sal C
Security (TACAS)
10:30 – 12:30, Stora Salen, 6th Floor
Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization
Publisher's Version Preprint Info
Inference and Evolution of TypeScript Declaration Files
Best-Paper Award Nominee
Publisher's Version Preprint Info
A Truly Concurrent Game Model of the Asynchronous π-Calculus
Publisher's Version
Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions
Best-Paper Award Nominee
Publisher's Version
Faster Algorithms for Weighted Recursive State Machines
Publisher's Version Preprint
Explicit Connection Actions in Multiparty Session Types
Publisher's Version
Local Model Checking in a Logic for True Concurrency
Publisher's Version Preprint
Discriminating Traces with Time
Publisher's Version Preprint
ML and Extended Branching VASS
Publisher's Version Preprint
Change and Delay Contracts for Hybrid System Component Verification
Publisher's Version Preprint Info
The Paths to Choreography Extraction
Publisher's Version Preprint
Directed Automated Memory Performance Testing
Publisher's Version Preprint Info
Modular Verification of Higher-Order Functional Programs
Publisher's Version
Precise Version Control of Trees with Line-Based Version Control Systems
Best-Paper Award Nominee
Publisher's Version Preprint Video Info
On the Undecidability of Asynchronous Session Subtyping
Publisher's Version Preprint
Context-Bounded Analysis for POWER
Best-Paper Award Nominee
Publisher's Version Preprint
Lunch
12:30 – 14:00, Sal D, Street Level
Theorem Proving (ESOP)
14:00 – 16:00, Sal B
Graph Modelling and Transformation (FASE)
14:00 – 16:00, Sal C
Competition on Software Verification (SV-COMP) (TACAS)
14:00 – 16:00, Stora Salen, 6th Floor
Comprehending Isabelle/HOL's Consistency
Publisher's Version Preprint
StaticGen: Static Generation of UML Sequence Diagrams
Publisher's Version
Software Verification with Validation of Results (Report on SV-COMP 2017)
Publisher's Version Preprint Info
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants
Publisher's Version Preprint Info
Inter-model Consistency Checking Using Triple Graph Grammars and Linear Optimization Techniques
Publisher's Version
AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (Competition Contribution)
Publisher's Version Preprint
Generalizing Inference Systems by Coaxioms
Publisher's Version Preprint Info
GTS Families for the Flexible Composition of Graph Transformation Systems
Publisher's Version
CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution)
Publisher's Version
Verified Characteristic Formulae for CakeML
Publisher's Version Preprint
Symbolic Model Generation for Graph Properties
Publisher's Version
DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs (Competition Contribution)
Publisher's Version Preprint
Forester: From Heap Shapes to Automata Predicates (Competition Contribution)
Publisher's Version Preprint Info
HipTNT+: A Termination and Non-termination Analyzer by Second-Order Abduction (Competition Contribution)
Publisher's Version
Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation (Competition Contribution)
Publisher's Version
Skink: Static Analysis of Programs in LLVM Intermediate Representation (Competition Contribution)
Publisher's Version
Symbiotic 4: Beyond Reachability (Competition Contribution)
Publisher's Version Preprint
Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)
Publisher's Version
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata (Competition Contribution)
Publisher's Version
Ultimate Taipan: Trace Abstraction and Abstract Interpretation (Competition Contribution)
Publisher's Version
VeriAbs: Verification by Abstraction (Competition Contribution)
Publisher's Version
Coffee Break
16:00 – 16:30, 3rd and 6th Floor
Compositional Testing (Tutorial)
16:30 – 18:00, Stora Salen, 6th Floor
Run-Time Verification and Logic (TACAS)
16:30 – 18:00, Sal B
Compositional Testing (Tutorial)
Ken McMillan
(Microsoft Research, USA)
Rewriting-Based Runtime Verification of Alternation-Free HyperLTL
Publisher's Version
Almost Event-Rate Independent Monitoring of Metric Temporal Logic
Publisher's Version Preprint
Optimal Translation of LTL to Limit Deterministic Automata
Publisher's Version Preprint Info
Friday, April 28, 2017
Fundamental Algorithmic Problems and Challenges in Dynamical and Cyber-Physical Systems (Invited Talk)
09:00 – 10:00, Stora Salen, 6th Floor
Fundamental Algorithmic Problems and Challenges in Dynamical and Cyber-Physical Systems (Invited Talk)
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
Model Transformations (FASE)
10:30 – 12:30, Sal C
Quantitative Systems 1 (TACAS)
10:30 – 12:30, Stora Salen, 6th Floor
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
Publisher's Version Preprint
Traceability Mappings as a Fundamental Instrument in Model Transformations
Publisher's Version Preprint
Sequential Convex Programming for the Efficient Verification of Parametric MDPs
Publisher's Version Preprint
Temporary Read-Only Permissions for Separation Logic
Publisher's Version Preprint Info
Reusing Model Transformations Through Typing Requirement Models
Publisher's Version Preprint
JANI: Quantitative Model and Tool Interaction
Publisher's Version
The Essence of Higher-Order Concurrent Separation Logic
Publisher's Version Preprint
Change-Preserving Model Repair
Publisher's Version Info
Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults
Publisher's Version Preprint Info
Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
Publisher's Version Preprint
A Deductive Approach for Fault Localization in ATL Model Transformations
Best-Paper Award Nominee
Publisher's Version Preprint Video Info
Long-Run Rewards for Markov Automata
Publisher's Version Preprint Info
Lunch
12:30 – 14:00, Sal D, Street Level
Session Types (ESOP)
14:00 – 16:00, Sal B
Configuration and Synthesis (FASE)
14:00 – 16:00, Sal C
SAT and SMT (TACAS)
14:00 – 16:00, Stora Salen, 6th Floor
Context-Free Session Type Inference
Best-Paper Award Nominee
Publisher's Version Preprint Info
OpenSAW: Open Security Analysis Workbench
Publisher's Version Info
HiFrog: SMT-based Function Summarization for Software Verification
Publisher's Version Info
Linearity, Control Effects, and Behavioural Types
Publisher's Version
Visual Configuration of Mobile Privacy Policies
Publisher's Version
Congruence Closure with Free Variables
Publisher's Version Preprint
Proving Linearizability Using Partial Orders
Publisher's Version
Automated Workarounds from Java Program Specifications Based on SAT Solving
Publisher's Version Preprint Info
On Optimization Modulo Theories, MaxSMT and Sorting Networks
Publisher's Version Preprint Info
The Power of Non-determinism in Higher-Order Implicit Complexity - Characterising Complexity Classes Using Non-deterministic Cons-Free Programming
Publisher's Version Preprint
Slicing from Formal Sematics: Chisel
Publisher's Version Preprint Info
The Automatic Detection of Token Structures and Invariants Using SAT Checking
Publisher's Version
EasyInterface: A Toolkit for Rapid Development of GUIs for Research Prototype Tools
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
Software Product Lines (FASE)
16:30 – 18:00, Sal C
Quantitative Systems 2 (TACAS)
16:30 – 18:00, Stora Salen, 6th Floor
A Classical Sequent Calculus with Dependent Types
Publisher's Version
Family-Based Model Checking with mCRL2
Publisher's Version
Maximizing the Conditional Expected Reward for Reaching the Goal
Publisher's Version Preprint
Lincx: A Linear Logical Framework with First-Class Contexts
Publisher's Version
Variability-Specific Abstraction Refinement for Family-Based Model Checking
Publisher's Version Preprint
ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans
Publisher's Version Preprint
Programs Using Syntax with First-Class Binders
Publisher's Version
A Unified and Formal Programming Model for Deltas and Traits
Publisher's Version
FlyFast: A Mean Field Model Checker
Publisher's Version
ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations
Publisher's Version Preprint Info

Time stamp: 2020-07-10T12:09:09+02:00