Programming Languages and Systems

Name: Programming Languages and Systems | 9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5-7, 2011. Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5-7, 2011. Proceedings

Hongseok Yang(Herausgeber*in)

Springer (Verlag)

Erschienen am 4. Dezember 2011

XI, 372 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-25318-8 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

Intro
Title Page
Preface
Organization
Table of Contents
Invited Talks
Program Analysis and Machine Learning: A Win-Win Deal
References
Software Verification with Liquid Types
Engineering Theories with Z3
Introduction
SMT, DPLL(T), and Z3
SMT
DPLL(T)
Z3's Theory Solver API
Weighted MaxSMT
Theories for Partial Orders and Class Inheritance
A Basic Solver for Partial Orders
Sub-typing Closure
A Theory of Object Graphs
An Encoding Using Arrays
An Encoding Using Recursive Data-Types and Arrays
Not All Encodings are Equal
HOL
Leveraging Theories
Conclusions
References
Algebra, Logic, Locality, Concurrency
References
Session 1: Program Analysis
Modular Abstractions of Reactive Nodes Using Disjunctive Invariants
Introduction
Invariants by Predicate Abstraction
Solution of a Universally Quantified Formula
Naive Algorithm for a Given Postcondition
Performance Improvements
Iterative Refinement of Invariants
Extensions
Step-by-Step Example of Invariant Inference
Construction of the Abstract Automaton
Related Work
Conclusion
Modular Abstractions of Reactive Nodes Using Disjunctive Invariants
Introduction
Invariants by Predicate Abstraction
Solution of a Universally Quantified Formula
Naive Algorithm for a Given Postcondition
Performance Improvements
Iterative Refinement of Invariants
Extensions
Step-by-Step Example of Invariant Inference
Construction of the Abstract Automaton
Related Work
Conclusion
References
Template-Based Unbounded Time Verification of Affine Hybrid Automata
Introduction
Basics
Our Approach: Getting into the Corset of the Monotone Framework
Adapting the Max-Strategy Approach
Conclusion
References
Access-Based Localization with Bypassing
Introduction
Setting: Analysis Framework
Graph Representation of Programs
Static Analysis
Access-Based Localization with Bypassing
Access-Based Localization: Previous Approach
Access-Based Localization with Bypassing: Our Approach
Delivery Points Optimization
Experiments
Setting Up
Results
Related Work
Conclusion
References
Session 2: Functional Programming
A Deductive Database with Datalog and SQL Query Languages
Introduction
System Architecture
Source-to-Source Program Transformations
Compile-Time Analyses
Strong Constraints
Tracing and Debugging
Conclusions
References
Constructing List Homomorphisms from Proofs
Introduction
Preliminaries
Folds and List Homomorphisms
From Duality to Homomorphism
The Steep List Problem
Constructing ( ) Formally
Computing Capacity by a List Homomorphism
Parallel Scan
Reasoning with Conditionals
Conclusions
References
Extending Hindley-Milner Type Inference with Coercive Structural Subtyping
Introduction
Notation and Terminology
Terms and Types
Subtyping and Coercions
Type Substitutions and Unification
Type Inference with Coercions
Coercive Subtyping Using Subtype Constraints
Constraint Generation
Constraint Simplification
Solving Subtype Constraints on a Graph
Coercion Insertion
Total Correctness and Completeness
An Example for Incompleteness
Complexity and Completeness
Related Work
Conclusion
References
Polymorphic Multi-stage Language with Control Effects
Introduction
Preliminaries
Introducing Polymorphism Safely
The Calculus
Type System
Type Soundness
Principal Type and Type Inference
Conclusion
References
Session 3: Compiler
Compiler Backend Generation for Application Specific Instruction Set Processors
Introduction
Design Overview
Background
Open64.
Olive.
Design Goals
Design Framework
OpenDL
Instruction Description
Common Information Extraction
Instruction Sharing
Pattern Abstraction
Rule Library
Terminal Declaration
Nonterminal Declaration
Grammar Rules
Mapping Rules
AutoAST
Experimental Results
OpenDL
Reliability
Performance of Embedded Benchmarks
Performance of Large-Scale Applications
Case Study: Design Space Exploration of ASIPs
Related Work
Conclusion
References
A Non-iterative Data-Flow Algorithmfor Computing Liveness Sets in Strict SSA Programs
Introduction
Related Work
Foundations
Control-Flow Graph and Loop Structure
Static Single Assignment Form
Liveness
Complexity of Liveness Algorithms
Computing Liveness Sets Using Loop-Nesting Forests
Liveness Sets on Reducible Control-Flow Graphs
Liveness Sets on Irreducible Control-Flow Graphs
Experiments
Conclusion
References
SPAS: Scalable Path-Sensitive Pointer Analysison Full-Sparse SSA
Introduction
Related Work
The Basic Idea
A Motivating Example
The SPAS Framework
Encoding Program Paths as BDDs
Extended SSA Form
Capturing Path Correlation
Supporting Strong Updates
Experimental Evaluation
Analysis Overhead
Path-Sensitive Precision
Conclusion
References
Session 4: Concurrency 1
On the Strength of Owicki-Gries for Resources
Introduction
Resource-Manipulating Language and Its Semantics
Language RPL
Semantics of RPL
Owicki-Gries-Core Proofs
Lattice of Owicki-Gries-Core Proofs
Examples
Owicki-Gries Core as Abstract Interpretation
Owicki-Gries-Core Proofs are the Post-Fixpoints of a Sound Abstract Successor Map
Characteristic Closures for Owicki-Gries Core?
Absence of Equivalent Characterizations by Closures
Upper Bound on Precision
Lower Bound on Precision
Simple Cartesian Closure
More Precise Lower Bound Closure
Related Work
Discussion
Challenges
Conclusion
References
Solving Recursion-Free Horn Clauses over LI+UIF
Introduction
Illustration
Recursion-Free Horn Clauses
Algorithm
Resolution Tree
Proof Tree
Annotated Proof Tree
Correctness and Complexity
Conclusion
References
Macro Tree Transformations of Linear Size Increase Achieve Cost-Optimal Parallelism
Introduction
Preliminary
Trees
Parallel Tree Contraction
Tree Transducers
Macro Tree Transducers
Strongly Single-Use Restricted MTTs
Top-Down Relabeling with Regular Lookahead
Parallel Evaluation of Tree Transformations
Parallel Evaluation of Top-Down Relabeling with Regular Lookaheads
Parallel Evaluation of Strongly Single-Use Restricted Macro Tree Transducers
Parallel Evaluation of Complicated Tree Transformations of Linear Size Increase
Macro Tree Transformations
Higher-Order Tree Transformations
Primitive Recursive Tree Transformations
Tree-Walking Transformations with Pebbles
Other Classes of Tree Transformations
Concluding Remarks
References
Decentralized Delimited Release
Introduction
Decentralized Delimited Release
Decentralized Policies
From DLM0 to Families of Indistinguishability Relations
Enforcement
Experiments
Related Work
Conclusion
References
Session 5: Concurrency 2
Cost Analysis of Concurrent OO Programs
Introduction
A Language with Concurrent Objects
A Rule-Based Intermediate Language
Cost and Cost Models for Concurrent Programs
The Basic Cost Analysis Framework
Field-Sensitive Size Analysis for Concurrent OO Programs
Cost Relations Based on Cost Centers
Class Invariants in Cost Analysis
Experiments: The COSTABS System
Conclusions and Related Work
References
Static Object Race Detection
Introduction
Formal Account of Object Graphs
Concrete Semantics
Abstract Semantics
Dominance Inference Analysis
Dominance Boundary
Minimal Boundaries
Object Race Detection
Reentrancy Analysis
Lock Analysis
Object Race Detection Analysis
Implementation
Related Work
Conclusions
References
Soundness of Data Flow Analyses for Weak Memory Models
Introduction
Background
Weak Memory Models
Programs vs. Event Structures
Soundness of Analyses on Weak Memory Models
Definition of Soundness
SC-Soundness Entails A-Soundness for Non-relational Analyses
Proving Soundness of Analyses over Programs
Repairing Unsound Analyses
Specification vs. Implementations of the Repair Loop
Related Work and Conclusion
References
Session 6: Semantics
Towards a Certified Petri Net Model-Checker
Introduction
Coloured Petri Nets
LLVM
Syntax and Intuitive Semantics
LLVM-Labelled Petri Nets
Implementing State Space Exploration
A Formal Semantics of LLVM
Memory Model
Inference Rules
Data Structures Interpretation
Correctness and Termination Results
Conclusion
References
Elementary Linear Logic Revisited for Polynomial Timeand an Exponential Time Hierarchy
Introduction
Characterization of the Classes P and k-EXP
Proof-Nets and Complexity Soundness
Extensional Completeness
Conclusion and Future Work
References
A Proof Pearl with the Fan Theorem and Bar Induction
Introduction
Preliminaries
Always Blue and Eventually Red Trees
Always Blue Trees
Eventually Red Trees
Eventually Always vs. Almost Always Blue Trees
Eventually Always Blue Trees
Almost Always Blue Trees
Always Eventually Red vs. Infinitely Often Red Trees
Existential Properties
Related Work
Conclusion
References
A Semantics for Context-Sensitive Reduction Semantics
Introduction
Matching and Contexts
A Semantics for Matching
An Algorithm for Matching
A Semantics for Reduction
Related Work
References
Towards a General Theory of Barbs, Contexts and Labels
Introduction
Two Case Studies
Mobile Ambients
HoCore
Reactive Systems and Context LTSs
Barbed Saturated Semantics
Weak Context Bisimilarity
Congruence Property
Weak L-Bisimilarity
Weak Barbed Saturated Bisimilarity via Weak L-Bisimilarity
Labelled Characterization for MAs Weak Semantics
Labelled Characterizations for HoCore Semantics
Conclusions and Future Work
References
Computation-by-Interaction with Effects
Weak Effect Calculus
Implementing Interaction
A Metalanguage for Interactive Computation
Models of the Weak Effect Calculus
Trace and Int-Construction
Interpreting the Metalanguage in WEC
Conclusion
References
Author Index

Inhalt (PDF)

Systemvoraussetzungen

Als PDF speichern Als Link merken