Preliminary Programme

1st Day, 28 Nov  |  2nd Day, 29 Nov  |  3rd Day, 30 Nov  |  4th Day, 1 Dec

27 November (Saturday)
10:00-20:00Registration (Hengshan Hotel)
28 November (Sunday)
9:00-14:00Registration (Hengshan Hotel)
14:30-16:00 Tutorial I: Probabilistic testing semantics
Yuxin Deng
16:00-16:30Coffee break
16:30-18:00 Tutorial II: A Logical Mix of Approximation and Separation
Aquinas Hobor and Robert Dockins
18:30 - 20:30 Reception

29 November (Monday)
9:00-9:15 Opening
9:15-10:15 Keynote Address  (Session Chair: Kazunori Ueda)
A Calculus for Hybrid CSP
ZHOU Chaochen
10:15-10:45Coffee break
10:45-12:15Session 1 (Session Chair: Sungwoo Park)

Typechecking Higher-Order Security Libraries
Karthikeyan Bhargavan, Cedric Fournet and Nataliya Guts

Deriving Type Systems and Implementations for Coroutines
Konrad Anton and Peter Thiemann

Liberal Typing for Functional Logic Programs
Francisco J. Lo'pez-Fraguas, Enrique Martin-Martin and Juan Rodriguez-Hortala
12:15 - 13:45Lunch break
13:45-15:15Session 2 (Session Chair: Zhenjiang Hu)

A Provably Correct Stackless Intermediate Representation for Java Bytecode
Delphine Demange, Thomas Jensen and David Pichardie

JNI Light: An Operational Model for the Core JNI
Gang Tan

An interactive tool for analyzing embedded SQL queries [system and tool presentation]
Aivar Annamaa, Andrey Breslav, Jevgeni Kabanov and Varmo Vene
15:15-15:45Coffee break
15:45-16:45 Invited talk 1  (Session Chair: Yuxi Fu)
Foundations of Quantum Programming
Mingsheng Ying
16:45-17:00Short break
17:00-18:00Session 3 (Session Chair: Kwangkeun Yi)

Simple and Precise Widenings for H-Polyhedra
Axel Simon and Liqian Chen

Metric Spaces and Termination Analyses
Aziem Chawdhary and Hongseok Yang

30 November (Tuesday)
9:00-10:00 Invited Talk 2  (Session Chair: Alwen Tiu)
From a Verified Kernel Towards Verified Systems
Gerwin Klein
10:00-10:30Coffee break
10:30-12:00Session 4 (Session Chair: Peter Thiemann)

Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics
Jan Hoffmann and Martin Hofmann

Interprocedural Control Flow Reconstruction
Andrea Flexeder, Helmut Seidl, Michael Petter and Bogdan Mihaila

Data Structure Fusion
Peter Hawkins, Alex Aiken, Kathleen Fisher, Martin Rinard and Mooly Sagiv
12:00 - 13:30Lunch break
13:30-15:00Session 5 (Session Chair: Jacques Garrigue)

Categorical Descriptional Composition
Shin-ya Katsumata

Bisimulation proof methods in a path-based specification language for polynomial coalgebras
Xiaocong Zhou, Yongji Li, Wenjun Li, Haiyan Qiao and Zhongmei Shu

Context-Preserving XQuery Fusion
Hiroyuki Kato, Soichiro Hidaka, Zhenjiang Hu, Keisuke Nakano and Yasunori Ishihara
15:00-15:30Coffee break
15:30-16:15Poster Session (Chair: Guoqiang Li)
16:15-17:15Session 6 (Session Chair: Hideya Iwasaki)

Index-Compact Garbage Collection
Liangliang Tong and Francis C.M. Lau

Live heap space bounds for real-time systems
Martin Kero, Pawel Pietrzak and Johan Nordlander

18:00 - 20:30 Banquet

1 December (Wednesday)
9:00-10:00 Invited Talk 3  (Session Chair: Sungwoo Park)
Reasoning about Computations Using Two-Levels of Logic
Dale Miller
10:00-10:30Coffee break
10:30-12:00Session 7 (Session Chair: Aquinas Hobor)

A Quick Tour of the VeriFast Program Verifier [system and tool presentation]
Bart Jacobs, Jan Smans and Frank Piessens

Verification of Tree-Processing Programs via Higher-Order Model Checking
Hiroshi Unno, Naoshi Tabuchi and Naoki Kobayashi

Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Templates
Soonho Kong, Yungbum Jung, Cristina David, Bow-yaw Wang and Kwangkeun Yi
12:00 - 13:30Lunch break
13:30-15:00Session 8 (Session Chair: Tyng-Ruey Chuang)

Relational Parametricity for a Polymorphic Linear Lambda Calculus
Jianzhou Zhao, Qi Zhang and Steve Zdancewic

A Certified Implementation of ML with Structural Polymorphism
Jacques Garrigue

Type Inference for Sublinear Space Functional Programming
Ugo Dal Lago and Ulrich Schoepp
15:00-15:30Coffee break
15:30-17:00Session 9 (Session Chair: Yuxin Deng)

Liveness of Communicating Transactions (Extended Abstract)
Edsko de Vries, Vasileios Koutavas and Matthew Hennessy

Model Independent Order Relations for Processes
Chaodong He

Concurrency Can't Be Observed, Asynchronously
Paolo Baldan, Filippo Bonchi, Fabio Gadducci and Giacoma Monreale

1st Day, 28 Nov  |  2nd Day, 29 Nov  |  3rd Day, 30 Nov  |  4th Day, 1 Dec