Schedule

The location of APLAS NIER Workshop and Conference is at Bali Room (from the hotel lobby, turn left and go downstair).
The location of poster session is at Puri Bali (from the hotel lobby, turn left and go downstair).
The location of PC chair report and lunch is at El Patio restaurant (from the hotel lobby, go downstair).
The location of banquet dinner is at Temple Garden.
Please see the map of the Melia Bali hotel at the lobby.


Sunday, 1 December
10:30 – 12:00APLAS NIER – Session 1

Towards Understanding and Reasoning about Android Interoperations
Sora Bae (Oracle Labs), Sungho Lee (KAIST), Sukyoung Ryu (KAIST)
A Survey on Technologies for Designing and Implementing Safe and Correct Distributed Software
Andreea Costea (National University Of Singapore)
A Constant-time Preserving C Compiler
Sandrine Blazy (Univ Rennes- IRISA)
12:00 – 13:30Catering – Lunch
13:30 – 15:00APLAS NIER – Session 2

On Probabilistic Process
Yuxi Fu (Shanghai Jiao Tong University
On Decidable Subtyping for Path Dependent Types
Julian Mackay (Victoria University of Wellington), Yu Xiang Zhu (Carnegie Mellon University), Alex Potanin (Victoria University of Wellington), Jonathan Aldrich (Carnegie Mellon University), Lindsay Groves (Victoria University of Wellington)
Word Equations with Length Constraints and Presburger Arithmetic with Divisibility
Anthony Widjaja Lin (Technische Universität Kaiserslautern), Rupak Majumdar (Max Planck Institute for Software Systems)
15:00 – 15:30Catering – Cofee Break
15:30 – 17:00APLAS NIER – Session 3

Label-Dependent Session Types
Peter Thiemann (University of Freiburg), Vasco Vasconcelos (University of Lisbon)
Space-Efficient Gradual Typing in Coercion-Passing Style
Atsushi Igarashi (Kyoto University), Yuya Tsuda (Kyoto University), Tomoya Tabuchi (Kyoto University)
The Polynomial Complexity of Vector Addition Systems with States
Florian Zuleger (TU Vienna)
Monday, 2 December
08:50 – 10:00Keynote Talks – Keynote 1
Chair(s): Anthony Widjaja Lin

Proving that Programs are Differentially Private
Annabelle McIver (Macquarie University)
10:00 – 10:30Catering – Coffee Break
10:30 – 12:00Research Papers – Types
Chair(s): Tachio Terauchi

Manifest Contracts with Intersection Types
Yuki Nishida (Kyoto University), Atsushi Igarashi (Kyoto University)
A Dependently Typed Multi-Stage Calculus
Akira Kawata (Kyoto University), Atsushi Igarashi (Kyoto University)
Existential Types for Relaxed Noninterference
Raimil Cruz (University of Chile), Éric Tanter (University of Chile)
12:00 – 13:30Catering – Lunch
13:30 – 15:00Research Papers – Program Analysis
Chair(s): Annabelle McIver

Dissecting Widening: Separating Termination from Information
Graeme Gange, Jorge A. Navas (SRI International), Peter Schachte, Harald Sondergaard, Peter J. Stuckey (Monash University)
A Type-Based HFL Model Checking Algorithm
Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada (University of Tokyo)
Reducing Static Analysis Alarms based on Non-impacting Control Dependencies
Tukaram Muske, Rohith Talluri (Tata Consultancy Services Ltd), Alexander Serebrenik (Eindhoven University of Technology)
15:00 – 15:30Catering – Coffee Break
15:30 – 17:00Research Papers – Semantics
Chair(s): Atsushi Igarashi

Factorization and Normalization, Essentially
Beniamino Accattoli (Inria & Ecole Polytechnique), Claudia Faggian (IRIF), Giulio Guerrieri (University of Bath)
Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion
Masayuki Mizuno, Eijiro Sumii (Tohoku University)
Recursion Schemes in Coq
Kosuke Murata (Kyushu Institute of Technology), Kento Emoto (University of Tokyo)
17:00 – 17:15PC Chair Report – PC Chair Report
18:00 – 20:00Poster Session
Chair(s): Andreea Costea
18:00 – 20:00Catering – Reception
Tuesday, 3 December
09:00 – 10:00Keynote Talks – Keynote 2
Chair(s): Anthony Widjaja Lin

Network Verification: Past, Present, and Future
Nate Foster (Cornell University)
10:00 – 10:30Catering – Coffee Break
10:30 – 12:00Research Papers – Language Design and Implementation
Chair(s): Éric Tanter

Lightweight Functional Logic Meta-Programming
Nada Amin (Harvard University), William E. Byrd (University of Alabama), USA, Tiark Rompf (Purdue University)
Mimalloc: Free List Sharding in Action
Daan Leijen, Ben Zorn, Leonardo De Moura (Microsoft Research)
LiFtEr: Language to Encode Induction Heuristics for Isabelle/HOL
Yutaka Nagashima (Czech Technical University & University of Innsbruck)
12:00 – 13:30Catering – Lunch
13:30 – 15:00Research Papers – Concurrency
Chair(s): Philipp Ruemmer

Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps
Taolue ChenBirkbeck (University of London), Jilong He (Chinese Academy of Sciences), Yu-Ping Wang (Tsinghua University), Zhilin Wu (Chinese Academy of Sciences), Jun Yan (Chinese Academy of Sciences)
Conflict Abstractions and Shadow Speculation for Optimistic Transactional Objects
Thomas Dickerson (Brown University), Paul Gazzillo (University of Central Florida), Maurice Herlihy (Brown University), Eric Koskinen (Stevens Institute of Technology)
Transactional Forest: A DSL for Managing Concurrent Filestores
Jonathan DiLorenzo (Cornell University), Kathryn Mancini (Cornell University), Kathleen Fisher (Tufts University), Nate Foster (Cornell University)
15:00 – 15:30Catering – Coffee Break
15:30 – 17:15Research Papers – Verification
Chair(s): Zhilin Wu

J-ReCoVer: Java Reducer Commutativity Verifier [Tool Paper]
Yu-Fang Chen (Academia Sinica), Chang-Yi Chiang (National Taipei University), Lukas Holik (Brno University of Technology), Wei-Tsung Kao (Academia Sinica), Hsin-Hung Lin (Academia Sinica), Yean-Fu Wen (National Taipei University), Tomas Vojnar (Brno University of Technology), Wei-Cheng Wu (Academia Sinica)
Uniform Random Process Model Revisited
Wenbo Zhang, Huan Long (Shanghai Jiao Tong University), Xian Xu (East China University of Science and Technology)
Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions
Makoto Tatsuta (National Institute of Informatics), Koji Nakazawa (Nagoya University), Daisuke Kimura (Toho University)
Compositional Verification of Heap-Manipulating Programs through Property-Guided Learning
Long H. Pham (Singapore University of Technology and Design), Jun Sun (Singapore Management University), Quang Loc Le (Teesside University)
18:00 – 21:00Catering – Banquet
Wednesday, 4 December
09:00 – 10:00Keynote Talks – Keynote 3
Chair(s): Anthony Widjaja Lin

On Strings in Software Model Checking
Philipp Ruemmer (Uppsala University)
10:00 – 10:30Catering – Coffee Break
10:30 – 12:00Research Papers – Logic and Automata
Chair(s): Peter Thiemann

Pumping, With or Without Choice
Aquinas Hobor (National University of Singapore), Elaine Li (Runtime Verification, Inc.), Frank Stephan (National University of Singapore)
Simulations in Rank-Based Buchi Automata Complementation
Yu-Fang Chen (Academia Sinica), Vojtěch Havlena (Brno University of Technology), Ondrej Lengal (Brno University of Technology)
Succinct Determinisation of Counting Automata via Sphere Construction
Lukas Holik (Brno University of Technology), Tomas Vojnar (Brno University of Technology), Ondrej Lengal (Brno University of Technology), Lenka Turonova (Brno University of Technology), Margus Veanes (Microsoft Research), Olli Saarikivi
12:00 – 13:30Catering – Lunch