ETAPS 2017 Thursday

Thursday, April 27, 2017

Plenary 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 Erik Krogh Kristensen and Anders Møller (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 Paolo Baldan and Tommaso Padoan (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 Sudipta Chattopadhyay (Saarland University, Germany) Publisher's Version Preprint Info
Modular Verification of Higher-Order Functional Programs Ryosuke Sato and Naoki Kobayashi (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

Lunch 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) Dirk Beyer (LMU Munich, Germany) Publisher's Version Preprint Info
Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel (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 Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, and Michael Norrish (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

Plenary 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