(Printable version here)

(temporary access to proceedings of the technical track will be available from Springer here)

Sunday (2nd December)

Workshop on New Ideas and Emerging Results (NIER’18)
11am: Session 1 : Decidability and Synthesis (Rutherford House LT2)
On The Decidability of PDA by Yuxi Fu
Transplanting Syntax-Guided Synthesis to Computer Networks by Xiaokang Qiu
12pm: Lunch (Pay Your Own @ Backbencher; RSVP here)
1:30pm: Session 2 : Programmability (Rutherford House LT2)
Bidirectional Programming in Datalog by Zhenjiang Hu
Task-Oriented Software Development with iTasks by Jurriën Stutterhei
Callability Control by Isaac Oscar Gariano and Marco Servetto
3pm: Afternoon Tea/Coffee
3:30pm: Session 3 : Specification & Verification (Rutherford House LT2)
Temporal Properties of Smart Contracts by Ilya Sergey, Amrit Kumar and Aquinas Hobor
On Cut-elimination in Cyclic Proof Systems by Daisuke Kimura, Koji Nakazawa, Tachio Terauchi and Hiroshi Unno
Metaprogramming Statically verified code by Hrshikesh Arora and Marco Servetto

Monday (3rd December)

8:30am: Welcome (Rutherford House LT2)
9am: Technical Track — Types (Rutherford House LT2)
Session Chair: Tachio Terauchi, Waseda University, Japan
Non-linear Pattern Matching with Backtracking for Non-free Data Types by Satoshi Egi (Rakuten Institute of Technology, Japan) and Yuichi Nishiwaki (University of Tokyo, Japan)
Types of Fireballs by Beniamino Accattoli (INRIA, France) and Giulio Guerrieri (University of Bologna, Italy)
Factoring Derivation Spaces via Intersection Types by Pablo Barenbaum (University of Buenos Aires, Argentina) and Gonzalo Ciruelos (Universidad de Buenos Aires, Argentina)
10:30am: Morning Tea/Coffee
11am: (Keynote) Amal Ahmed, “Compositional Compiler Verification for a Multi-Language World”
12pm Lunch (provided @ Rutherford House, Mezzanine Floor)
1:30pm Technical Track — Program Analysis (Rutherford House LT2)
Session Chair: Sukyoung Ryu, KAIST, South Korea
On the Soundness of Call Graph Construction in the Presence of Dynamic Language Features – A Benchmark and Tool Evaluation by Li Sui (Massey University, New Zealand), Jens Dietrich (Massey University, New Zealand), Amjed Tahir (Massey University, New Zealand), Shawn Rasheed (Massey University, New Zealand), and Michael Emery (Massey University, New Zealand)
Complexity Analysis of Tree Share Structure by Xuan Bach Le (National University of Singapore, Singapore), Aquinas Hobor (National University of Singapore, Singapore), and Anthony Widjaja Lin (University of Oxford, UK)
Relational Thread-Modular Abstract Interpretation Under Relaxed Memory Model by Thibault Suzanne (École Normale Supérieure, France) and Antoine Miné (LIP6, UPMC, France)
3pm: Afternoon Tea/Coffee
3:30pm Tool Papers (Rutherford House LT2)
Session Chair: Aquinas Hobor, National University of Singapore, Singapore
Scallina: Translating Verified Programs from Coq to Scala by Youssef El Bakouny (Saint-Joseph University of Beirut, Lebanon) and Dani Mezher (Saint-Joseph University of Beirut, Lebanon)
HoIce: A ICE-based Non-Linear Horn Clause Solver by Adrien Champion (University of Tokyo, Japan), Naoki Kobayashi (University of Tokyo, Japan), and Ryosuke Sato (Kyushu University, Japan)
Traf: a Graphical Proof Tree Viewer Cooperating with Coq through Proof General by Hideyuki Kawabata (Hiroshima City University, Japan), Yuta Tanaka (Hiroshima City University, Japan), Mai Kimura (Hiroshima City University, Japan), and Tetsuo Hironaka (Hiroshima City University, Japan)
The Practice of a Compositional Functional Programming Language by Timothy Jones (Montoux, New Zealand) and Michael Homer (Victoria University of Wellington, New Zealand)
6pm Poster Session

Tuesday (4th December)

9am: Technical Track —- Functional Programs and Probabilistic Programs (Rutherford House LT2)
Session Chair: Kenichi Asai, Ochanomizu University, Japan
New Approaches for Almost-Sure Termination of Probabilistic Programs by Mingzhang Huang (Shanghai Jiao Tong University, China), Hongfei Fu (Shanghai Jiao Tong University, China), and Krishnendu Chatterjee (IST Austria, Austria)
Particle-Style Geometry of Interaction as a Module System by Ulrich Schöpp (Ludwig Maximilian Universität München, Germany)
Automated Synthesis of Functional Programs with Auxiliary Functions by Shingo Eguchi (University of Tokyo, Japan), Naoki Kobayashi (University of Tokyo, Japan), and Takeshi Tsukada (University of Tokyo, Japan)
10:30am: Morning Tea/Coffee
11am: (Keynote) Azalea Raad, “Correctness in a weakly consistent setting”
12pm Lunch (provided @ Rutherford House, Mezzanine Floor)
1:30pm Pickup for excursion to Weta Digitial.
5pm Drop off at Te Papa, time to explore!
6:30pm Evening Banquet at Te Papa

Wednesday (5th December)

9am: Technical Track — Verification (Rutherford House LT2)
Session Chair: Chung-Kil Hur, Seoul National University, South Korea
Modular Verification of SPARCv8 Code by Junpeng Zha (University of Science and Technology of China, China), Xinyu Feng (Nanjing University, China), and Lei Qiao (Beijing Institute of Control Engineering, China)
Formal Verification of a Call-by-value Lambda Calculus Machine by Fabian Kunze (Saarland University, Germany), Gert Smolka (Saarland University, Germany), and Yannick Forster (Saarland University, Germany)
Automated Modular Verification for Relaxed Communication Protocols by Andreea Costea (National University of Singapore, Singapore), Wei-Ngan Chin (National University of Singapore, Singapore), Shengchao Qin (Teesside University, UK), and Florin Craciun (Babes-Bolyai University, Romania)
10:30am: Morning Tea/Coffee
11am: (Keynote) Bernhard Scholz, Soufflé: A Datalog Engine for Static Analysis
12pm Lunch (provided @ Rutherford House, Mezzanine Floor)
1:30pm Technical Track — Logic (Rutherford House LT2)
Session Chair: Wei Ngan Chin, National University of Singapore, Singapore
Automated proof synthesis for the minimal propositional logic with deep neural networks by Taro Sekiyama (National Institute of Informatics, Japan) and Kohei Suenaga (Kyoto University, Japan)
On the Complexity of Pointer Arithmetic in Separation Logic by James Brotherston (University College London, UK) and Max Kanovich (University College London, UK)
A Decision Procedure for String Logic with Quadratic Equations, Regular Expressions and Length Constraints by Quang Loc Le (Teesside University, UK) and Mengda He (Teesside University, UK)
3pm: Afternoon Tea/Coffee
3:30pm Continuation and Model Checking (Rutherford House LT2)
Session Chair: Atsushi Igarashi, Kyoto University, Japan
Certifying CPS Transformation of Let-polymorphic Calculus Using PHOAS by Urara Yamada (Ochanomizu University, Japan) and Kenichi Asai (Ochanomizu University, Japan)
Model Checking Differentially Private Properties by Depeng Liu (Chinese Academy of Science, China), Bow-Yaw Wang (Academia Sinica, Taiwan), and Lijun Zhang (Chinese Academy of Science, China)
Shallow Effect Handlers by Daniel Hillerström (University of Edinburgh, UK) and Sam Lindley (University of Edinburgh, UK)
5pm Closing

Thursday (6th December)

Sydney Area Programming Languages Interest Group (SAPLING’18)
8:50am Welcome (Rutherford House LT2)
9am Portable Memory Management Toolkit in Rust, Zixian Cai, Brenda Wang, Pavel Zakopaylo (Australian National University)
Understanding & Analysing the G1 Family of Garbage Collectors, Wenyu Zhao (Australian National University)
Using Program Analysis for Detecting Denial of Service (DoS) Vulnerabilities in Java Code, Shawn Rasheed (Massey University) and Jens Dietrich (Victoria University of Wellington)
10:30am Morning Tea / Coffee
11am (Keynote) On the Architecture of a (Verifying) Compiler, David Pearce (Victoria University of Wellington)
12pm Lunch (provided @ Rutherford House, Mezzanine Floor)
1:30pm (Keynote) The DaCapo Benchmark Suite: A Methodological, Engineering, and Social Journey, Steve Blackburn (Australian National University)
2:30pm What Programming Languages Do Developers Use? A Theory of Static vs Dynamic Language Choice, Aaron Pang, Craig Anslow and James Noble (Victoria University of Wellington)
3pm Afternoon Tea/Coffee
3:30pm Construction of Control Flow Graphs for Binary Programs, Dominik Klumpp (University of Augsburg, the Technical University Munich and the Ludwig-Maximilians-University Munich), Franck Cassez (Macquarie University)
Use of LINQ queries in C#, Erin Greenwood-Thessman, Michael Homer and James Noble (Victoria University of Wellington)
The Bounded Lattice Type System, Robert Smart
Nested Trait Composition for Modular Software Development, Marco Servetto (Victoria University of Wellington)
Declarative Specification of Indentation Rules: A Tooling Perspective on Parsing and Pretty-Printing Layout-Sensitive Languages, Luís Eduardo de Souza Amorim (TU Delft)
6pm Closing

Friday (7th December)

10am – 3pm: Software Innovation NZ Meeting