This book constitutes the refereed proceedings of the 7th Asian Symposium on Programming Languages and Systems, APLAS 2009, held in Seoul, Korea, in December 2009.
The 21 papers presented in this volume together with 3 invited talks were carefully reviewed and selected from 56 submissions. The papers are divided into topical sections on program analysis, transformation and optimization, type system, separation logic, logic and foundation theory, software security and verification, and software security and verification.
Author(s): Koen Claessen (auth.), Zhenjiang Hu (eds.)
Series: Lecture Notes in Computer Science 5904 : Programming and Software Engineering
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2009
Language: English
Pages: 359
Tags: Programming Languages, Compilers, Interpreters; Software Engineering; Logics and Meanings of Programs; Systems and Data Security; Programming Techniques; Mathematical Logic and Formal Languages
Front Matter....Pages -
The Twilight Zone: From Testing to Formal Specifications and Back Again....Pages 1-1
Types and Recursion Schemes for Higher-Order Program Verification....Pages 2-3
The Sketching Approach to Program Synthesis....Pages 4-13
Large Spurious Cycle in Global Static Analyses and Its Algorithmic Mitigation....Pages 14-29
Abstract Transformers for Thread Correlation Analysis....Pages 30-46
Scalable Context-Sensitive Points-to Analysis Using Multi-dimensional Bloom Filters....Pages 47-62
A Short Cut to Optimal Sequences....Pages 63-78
A Skeletal Parallel Framework with Fusion Optimizer for GPGPU Programming....Pages 79-94
Witnessing Purity, Constancy and Mutability....Pages 95-110
On the Decidability of Subtyping with Bounded Existential Types....Pages 111-127
Fractional Ownerships for Safe Memory Deallocation....Pages 128-143
Ownership Downgrading for Ownership Types....Pages 144-160
A Fresh Look at Separation Algebras and Share Accounting....Pages 161-177
Weak updates and separation logic....Pages 178-193
Proving Copyless Message Passing....Pages 194-209
On Stratified Regions....Pages 210-225
Parallel Reduction in Resource Lambda-Calculus....Pages 226-242
Classical Natural Deduction for S4 Modal Logic....Pages 243-258
Bi-abductive Resource Invariant Synthesis....Pages 259-274
Certify Once, Trust Anywhere: Modular Certification of Bytecode Programs for Certified Virtual Machine....Pages 275-293
Asymptotic Resource Usage Bounds....Pages 294-310
The Higher-Order, Call-by-Value Applied Pi-Calculus....Pages 311-326
Branching Bisimilarity between Finite-State Systems and BPA or Normed BPP Is Polynomial-Time Decidable....Pages 327-342
Refining Abstract Interpretation-Based Static Analyses with Hints....Pages 343-358
Back Matter....Pages -
