(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 |