The Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009)
13th Annual Asian Computing Science Conference (ASIAN 2009)
Seoul, Korea
14-16 December 2009
Venue: Room B103, Bldg Number 39 (BK Conference Hall), Seoul National University
Contact: aplas09 at ropas.snu.ac.kr

Program

Day 0: December 13, 2009 (Sunday)

09:00 - 10:30 Tutorial 1 Part 1

Separation Logic from the Perspective of Program Analysis
  Hongseok Yang (Queen Mary, University of London)

10:30 - 11:00 Break

11:00 - 12:30 Tutorial 1 Part 2

Separation Logic from the Perspective of Program Analysis
  Hongseok Yang (Queen Mary, University of London)

12:30 - 14:00 Lunch

14:00 - 15:30 Tutorial 2 Part 1

Parallel Programming in Fortress
  Sukyoung Ryu (Sun Microsystems Laboratories)

15:30 - 16:00 Break

16:00 - 17:30 Tutorial 2 Part 2

Parallel Programming in Fortress
  Sukyoung Ryu (Sun Microsystems Laboratories)

18:00 - 20:00 Conference Reception

Hoam Faculty House, Room Marronnier

Day 1: December 14, 2009 (Monday)

08:45 - 09:00 Opening

09:00 - 10:00 APLAS Invited Talk 1

The Sketching Approach to Program Synthesis
  Armando Solar-Lezama (MIT)

10:00 - 10:20 Break

10:20 - 11:50 APLAS Session 1: Program Analysis

Large Spurious Cycle in Global Static Analyses and Its Algorithmic Mitigation
  Hakjoo Oh
Abstract Transformers for Thread Correlation Analysis
  Michal Segalov, Tal Lev-Ami, Roman Manevich, Ramalingam Ganesan and Mooly Sagiv
Scalable Context-Sensitive Points-To Analysis using Multi-Dimensional Bloom Filters
  Rupesh Nasre, Kaushik Rajan, R. Govindarajan and Uday P. Khedker

12:00 - 13:30 Lunch

13:30 - 15:00 APLAS Session 2: Transformation and Optimization

A Short Cut to Optimal Sequences
  Akimasa Morihata
A Skeletal Parallel Framework with Fusion Optimizer for GPGPU Programming
  Shigeyuki Sato and Hideya Iwasaki
Witnessing Purity, Constancy and Mutability
  Ben Lippmeier

15:00 - 15:20 Break

15:20 - 16:50 APLAS Session 3: Type System

On the Decidability of Subtyping with Bounded Existential Types
  Stefan Wehr and Peter Thiemann
Fractional Ownerships for Safe Memory Deallocation
  Kohei Suenaga and Naoki Kobayashi
Ownership Downgrading for Ownership Types
  Yi Lu, John Potter and Jingling Xue

16:50 - 17:10 Break

17:10 - 18:10 APLAS Poster Session

An Order-sensitive Fusion for XQuery
  Hiroyuki Kato, Soichiro Hidaka, Zhenjiang Hu, Keisuke Nakano and Yasunori Ishihara
Derivation of a Linear-Time Algorithm for the Maximum Density Segment Problem
  Shin-Cheng Mu and Sharon Curtis
Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction
  Yungbum Jung, Soonho Kong, Bow-Yaw Wang and Kwangkeun Yi
Effective Generation of Quantified Boolean Verification Conditions for Non-Deterministic Boolean Programs
  Nikolay V. Shilov
Error Obliviating C Parser
  Yoonseok Ko
GRoundTram: A Bidirectional Graph Transformation System Based on Structural Recursion
  Soichiro Hidaka, Zhenjiang Hu, Kazuhiro Inaba, Hiroyuki Kato, Kazutaka Matsuda and Keisuke Nakano
PaI: A Grammar-Based Program Inversion System
  Kazutaka Matsuda
Shape Checking by Abstract Parsing & Enumeration
  Woosuk Lee, Heejung Kim and Kwangkeun Yi
Testing First-Order Logic Axioms in AutoCert
  Ki Yung Ahn and Ewen Denney

Day 2: December 15, 2009 (Tuesday)

09:00 - 10:00 APLAS Invited Talk 2

The Twilight Zone: From Testing to Formal Specifications and Back Again
  Koen Claessen (Chalmers University of Technology)

10:00 - 10:20 Break

10:20 - 11:50 APLAS Session 4: Separation Logic

A Fresh Look at Separation Algebras and Share Accounting
  Robert Dockins, Aquinas Hobor and Andrew W. Appel
Weak updates and separation logic
  Gang Tan, Zhong Shao, Xinyu Feng and Hongxu Cai
Proving Copyless Message Passing
  Jules Vil lard, Etienne Lozes and Cristiano Calcagno

12:00 - 13:30 Lunch

13:30 - 15:00 APLAS Session 5: Logic and Foundation Theory

On Stratified Regions
  Roberto M. Amadio
Parallel Reduction in Resource Lambda-Calculus
  Michele Pagani and Paolo Tranquil li
Classical Natural Deduction for S4 Modal Logic
  Daisuke Kimura and Yoshihiko Kakutani

15:00 - 15:20 Break

15:20 - 16:50 APLAS Session 6: Software Security and Verification (1)

Bi-Abductive Resource Invariant Synthesis
  Cristiano Calcagno, Dino Distefano and Viktor Vafeiadis
Certify Once, Trust Anywhere: Modular Certification of Bytecode Programs for Certified Virtual Machine
  Yuan Dong, Kai Ren, Shengyuan Wang and Suqin Zhang
Asymptotic Resource Usage Bounds
  Elvira Albert, Diego Alonso, Puri Arenas, Samir Genaim and German Puebla

16:50 - 17:10 Break

17:10 - 18:40 APLAS Session 7: Software Security and Verification (2)

The Higher-Order, Call-by-Value Applied Pi-Calculus
  Nobuyuki Sato and Eijiro Sumii
Branching Bisimilarity between Finite-State Systems and BPA or Normed BPP Is Polynomial-Time Decidable
  Hongfei Fu
Refining Abstract Interpretation-based Static Analyses with Hints
  Vincent Laviron and Francesco Logozzo

20:00 - 22:00 Conference Banquet

Day 3: December 16, 2009 (Wednesday)

09:00 - 10:30 APLAS/ASIAN Invited Talk

Part I: Types and Recursion Schemes for Higher-Order Program Verification
Part II: Higher-Order Program Verification and Language-Based Security
  Naoki Kobayashi (Tohoku University)

10:30 - 10:50 Break

10:50 - 11:50 ASIAN Session 1: Short Papers

A Dolev - Yao Model for Zero Knowledge
  Bhaskar Anguraj, R. Ramanujam and S. P. Suresh
Automated Security Proof for Symmetric Encryption Modes
  Martin Gagné, Pascal Lafourcade, Yassine Lakhnech and Reihaneh Safavi-Naini
Putting Chaos into Cryptography: A Critique of Chaotic-Map Based Stream Ciphers
  Matt Henricksen

12:00 - 13:30 Lunch

13:30 - 14:30 ASIAN invited talk

"Logic Wins!"
  Jean Goubault-Larrecq

14:30 - 16:00 ASIAN Session 2: Cryptography and System Security

A Simulation-Based Treatment of Authenticated Message Exchange
  Klaas Ole Kürtz, Henning Schnoor and Thomas Wilke
A Special Proxy Signature Scheme with Multi-Warrant
  Jianhong Zhang
Trusted Deployment of Virtual Execution Environment in Grid Systems
  Jinjiu Long, Deqing Zou and Hai Jin

16:00 - 16:20 Break

16:20 - 18:20 ASIAN Session 3: Security Foundations

Noninterference with Dynamic Security Domains and Policies
  Robert Grabowski and Lennart Beringer
A Logic for Formal Verification of Quantum Programs
  Yoshihiko Kakutani
Reducing Equational Theories for the Decision of Static Equivalence
  Steve Kremer, Antoine Mercier and Ralf Treinen
Deducibility constraints
  Sergiu Bursuc, Hubert Comon-Lundh and Stephanie Delaune