PLDI '15- Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Full Citation in the ACM Digital Library

SESSION: Distinguished Papers

Automatically improving accuracy for floating point expressions

Diagnosing type errors with class

Provably correct peephole optimizations with alive

SESSION: Correctness

Algorithmic debugging of real-world haskell programs: deriving dependencies from the cost centre stack

Automatic error elimination by horizontal code transfer across multiple applications

Light: replay via tightly bounded recording

Many-core compiler fuzzing

SESSION: Verification

Mechanized verification of fine-grained concurrent programs

Verification of producer-consumer synchronization in GPU programs

Relaxing safely: verified on-the-fly garbage collection for x86-TSO

Verifying read-copy-update in a logic for weak memory

SESSION: Optimization

LaminarIR: compile-time queues for structured streams

Optimizing off-chip accesses in multicores

Improving compiler scalability: optimizing large programs at small price


Verification of a cryptographic primitive: SHA-256 (abstract)

SESSION: Concurrency I

Asynchronous programming, analysis and testing with state machines

Stateless model checking concurrent programs with maximal causality reduction

Synthesizing racy tests

The Push/Pull model of transactions

SESSION: Synthesis I

Efficient synthesis of network updates

Efficient synthesis of probabilistic programs

FlashRelate: extracting relational data from semi-structured spreadsheets using examples

Synthesizing data structure transformations from input-output examples

SESSION: Concurrency II

Composing concurrency control

Dynamic partial order reduction for relaxed memory models

Monitoring refinement via symbolic reasoning

Preventing glitches and short circuits in high-level self-timed chip specifications

SESSION: Analysis

DAG inlining: a decision procedure for reachability-modulo-theories in hierarchical programs

Exploring and enforcing security guarantees via program dependence graphs

Making numerical program analysis fast

Tree dependence analysis

SESSION: Semantics I

A formal C memory model supporting integer-pointer casts

Defining the undefinedness of C

KJS: a complete formal semantics of JavaScript

Verdi: a framework for implementing and formally verifying distributed systems

SESSION: Performance

Static detection of asymptotic performance bugs in collection traversals

Autotuning algorithmic choice for input sensitivity

Helium: lifting high-performance stencil kernels from stripped x86 binaries to halide DSL code

Profile-guided meta-programming

SESSION: Semantics II

Declarative programming over eventually consistent data stores

Blame and coercion: together again for the first time

Lightweight, flexible object-oriented generics

Relatively complete counterexamples for higher-order programs


Automatic induction proofs of data-structures in imperative programs

Compositional certified resource bounds

Peer-to-peer affine commitment using bitcoin

Termination and non-termination specification inference

SESSION: Parallelism

Celebrating diversity: a mixture of experts approach for runtime mapping in dynamic environments

Efficient execution of recursive programs on commodity vector hardware

Loop and data transformations for sparse matrix code

Synthesizing parallel graph programs via automated planning

SESSION: Potpourri

Zero-overhead metaprogramming: reflection and metaobject protocols fast and without compromises

Finding counterexamples from parsing conflicts

Interactive parser synthesis by example

A simpler, safer programming and execution model for intermittent systems

SESSION: Synthesis II

Concurrency debugging with differential schedule projections

Synthesis of machine code from semantics

Synthesis of ranking functions using extremal counterexamples

Type-and-example-directed program synthesis