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

ETAPS 2017 Thursday

Thursday, April 27, 2017

09:00 – 10:00, Stora Salen, 6th Floor
Invited Talk: Natural language is a programming language
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
Session chair: Tachio Terauchi
Program and System Analysis (FASE)
10:30 – 12:30, K3+K4
Session chair: Einar Broch Johnsen
Concurrency (FOSSACS)
10:30 – 12:30, Sal C
Session chair: Javier Esparza
Security (TACAS)
10:30 – 12:30, Stora Salen, 6th Floor
Session chair: Gerardo Schneider
Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization
Hao Tang, Di Wang, Yingfei Xiong, Lingming Zhang, Xiaoyin Wang, and Lu Zhang
(Peking University, China; University of Texas at Dallas, USA; University of Texas at San Antonio, USA)
Publisher's Version Preprint Info
Inference and Evolution of TypeScript Declaration Files
(Aarhus University, Denmark)
Best-Paper Award Nominee
Publisher's Version Preprint Info
A Truly Concurrent Game Model of the Asynchronous π-Calculus
Ken Sakayori and Takeshi Tsukada
(University of Tokyo, Japan)
Publisher's Version
Static Detection of DoS Vulnerabilities in Programs that Use Regular Expressions
Valentin Wüstholz, Oswaldo Olivo, Marijn J. H. Heule, and Isil Dillig
(University of Texas at Austin, USA)
Best-Paper Award Nominee
Publisher's Version
Faster Algorithms for Weighted Recursive State Machines
Krishnendu Chatterjee, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis
(IST Austria, Austria; IIT Bombay, India)
Publisher's Version Preprint
Explicit Connection Actions in Multiparty Session Types
Raymond Hu and Nobuko Yoshida
(Imperial College London, UK)
Publisher's Version
Local Model Checking in a Logic for True Concurrency
(University of Padua, Italy)
Publisher's Version Preprint
Discriminating Traces with Time
Saeid Tizpaz-Niari, Pavol Cerný, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Ashutosh Trivedi
(University of Colorado at Boulder, USA)
Publisher's Version Preprint
ML and Extended Branching VASS
Conrad Cotton-Barratt, Andrzej S. Murawski, and C.-H. Luke Ong
(University of Oxford, UK; University of Warwick, UK)
Publisher's Version
Change and Delay Contracts for Hybrid System Component Verification
Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, and André Platzer
(JKU Linz, Austria; Carnegie Mellon University, USA)
Publisher's Version Preprint Info
The Paths to Choreography Extraction
Luís Cruz-Filipe, Kim S. Larsen, and Fabrizio Montesi
(University of Southern Denmark, Denmark)
Publisher's Version Preprint
Directed Automated Memory Performance Testing
(Saarland University, Germany)
Publisher's Version Preprint Info
Modular Verification of Higher-Order Functional Programs
(University of Tokyo, Japan)
Publisher's Version
Precise Version Control of Trees with Line-Based Version Control Systems
Dimitar Asenov, Balz Guenat, Peter Müller, and Martin Otth
(ETH Zurich, Switzerland; Ergon Informatik, Switzerland)
Best-Paper Award Nominee
Publisher's Version Preprint Video Info
On the Undecidability of Asynchronous Session Subtyping
Julien Lange and Nobuko Yoshida
(Imperial College London, UK)
Publisher's Version Preprint
Context-Bounded Analysis for POWER
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo
(Uppsala University, Sweden; University of Paris Diderot, France)
Best-Paper Award Nominee
Publisher's Version Preprint

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

Theorem Proving (ESOP)
14:00 – 16:00, Sal B
Session chair: Tachio Terauchi
Graph Modelling and Transformation (FASE)
14:00 – 16:00, Sal C
Session chair: Gabrielle Taentzer
Competition on Software Verification (SV-COMP) (TACAS)
14:00 – 16:00, Stora Salen, 6th Floor
Comprehending Isabelle/HOL's Consistency
Ondřej Kunčar and Andrei Popescu
(TU Munich, Germany; Middlesex University, UK)
Publisher's Version Preprint
StaticGen: Static Generation of UML Sequence Diagrams
Chris Alvin, Brian Peterson, and Supratik Mukhopadhyay
(Bradley University, USA; Louisiana State University, USA)
Publisher's Version
Software Verification with Validation of Results (Report on SV-COMP 2017)
(LMU Munich, Germany)
Publisher's Version Preprint Info
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants
(Inria, France; LORIA, France; Max Planck Institute for Informatics, Germany; École Polytechnique, France; ETH Zurich, Switzerland; Middlesex University, UK)
Publisher's Version Preprint Info
Inter-model Consistency Checking Using Triple Graph Grammars and Linear Optimization Techniques
Erhan Leblebici, Anthony Anjorin, and Andy Schürr
(TU Darmstadt, Germany; University of Paderborn, Germany)
Publisher's Version
AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (Competition Contribution)
Jera Hensel, Frank Emrich, Florian Frohn, Thomas Ströder, and Jürgen Giesl
(RWTH Aachen University, Germany)
Publisher's Version Preprint
Generalizing Inference Systems by Coaxioms
Davide Ancona, Francesco Dagnino, and Elena Zucca
(University of Genoa, Italy)
Publisher's Version Preprint Info
GTS Families for the Flexible Composition of Graph Transformation Systems
Steffen Zschaler and Francisco Durán
(King's College London, UK; University of Málaga, Spain)
Publisher's Version
CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution)
Pavel Andrianov, Karlheinz Friedberger, Mikhail U. Mandrykin, Vadim S. Mutilin, and Anton Volkov
(ISP RAS, Russia; University of Passau, Germany)
Publisher's Version
Verified Characteristic Formulae for CakeML
(ENS Lyon, France; Chalmers University of Technology, Sweden; Data61 at CSIRO, Australia)
Publisher's Version Preprint
Symbolic Model Generation for Graph Properties
Sven Schneider, Leen Lambers, and Fernando Orejas
(HPI, Germany; Universitat Politècnica de Catalunya, Spain)
Publisher's Version
DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs (Competition Contribution)
Williame Rocha, Herbert Rocha, Hussama Ismail, Lucas C. Cordeiro, and Bernd Fischer
(Federal University of Amazonas, Brazil; Federal University of Roraima, Brazil; University of Oxford, UK; Stellenbosch University, South Africa)
Publisher's Version Preprint
Forester: From Heap Shapes to Automata Predicates (Competition Contribution)
Lukás Holík, Martin Hruska, Ondrej Lengál, Adam Rogalewicz, Jirí Simácek, and Tomás Vojnar
(Brno University of Technology, Czech Republic)
Publisher's Version Preprint Info
HipTNT+: A Termination and Non-termination Analyzer by Second-Order Abduction (Competition Contribution)
Ton Chanh Le, Quang-Trung Ta, and Wei-Ngan Chin
(National University of Singapore, Singapore)
Publisher's Version
Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation (Competition Contribution)
Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato
(University of Southampton, UK; Stellenbosch University, South Africa; University of Salerno, Italy)
Publisher's Version
Skink: Static Analysis of Programs in LLVM Intermediate Representation (Competition Contribution)
Franck Cassez, Anthony M. Sloane, Matthew Roberts, Matthew Pigram, Pongsak Suvanpong, and Pablo González de Aledo Marugán
(Macquarie University, Australia; University of Cantabria, Spain)
Publisher's Version
Symbiotic 4: Beyond Reachability (Competition Contribution)
Marek Chalupa, Martina Vitovská, Martin Jonáš, Jiri Slaby, and Jan Strejcek
(Masaryk University, Czech Republic)
Publisher's Version Preprint
Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)
Jan Mrázek, Martin Jonáš, Vladimír Štill, Henrich Lauko, and Jiří Barnat
(Masaryk University, Czech Republic)
Publisher's Version
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata (Competition Contribution)
Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus, Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling, Frank Schüssele, and Andreas Podelski
(University of Freiburg, Germany)
Publisher's Version
Ultimate Taipan: Trace Abstraction and Abstract Interpretation (Competition Contribution)
Marius Greitschus, Daniel Dietsch, Matthias Heizmann, Alexander Nutz, Claus Schätzle, Christian Schilling, Frank Schüssele, and Andreas Podelski
(University of Freiburg, Germany)
Publisher's Version
VeriAbs: Verification by Abstraction (Competition Contribution)
Bharti Chimdyalwar, Priyanka Darke, Avriti Chauhan, Punit Shah, Shrawan Kumar, and R. Venkatesh
(Tata Consultancy Services, India)
Publisher's Version

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

16:30 – 18:00, Stora Salen, 6th Floor
Run-Time Verification and Logic (TACAS)
16:30 – 18:00, Sal B
Session chair: Wolfgang Ahrendt
Tutorial: Compositional Testing
Kenneth McMillan
(Microsoft Research, USA)
Rewriting-Based Runtime Verification of Alternation-Free HyperLTL
Noel Brett, Umair Siddique, and Borzoo Bonakdarpour
(McMaster University, Canada)
Publisher's Version
Almost Event-Rate Independent Monitoring of Metric Temporal Logic
David A. Basin, Bhargav Nagaraja Bhatt, and Dmitriy Traytel
(ETH Zurich, Switzerland)
Publisher's Version Preprint
Optimal Translation of LTL to Limit Deterministic Automata
Dileep Kini and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version Preprint Info