David Grove, Steve Blackburn
Proceedings of the 36th Conference on Programming Language Design and Implementation
PLDI, 2015.

@proceedings{PLDI-2015,
	acmid         = "2737924",
	address       = "Portland, Oregon, USA",
	editor        = "David Grove and Steve Blackburn",
	isbn          = "978-1-4503-3468-6",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 36th Conference on Programming Language Design and Implementation}",
	year          = 2015,
}

Contents (59 items)

11 ×#source code
6 ×#named
6 ×#performance
6 ×#synthesis
5 ×#verification
4 ×#automation
4 ×#concurrent
3 ×#debugging
3 ×#dependence
3 ×#graph

PLDI-2015-PanchekhaSWT #automation #float

Automatically improving accuracy for floating point expressions (PP, ASS, JRW, ZT), pp. 1–11.

PLDI-2015-ZhangMVJ #fault

Diagnosing type errors with class (DZ, ACM, DV, SLPJ), pp. 12–21.

PLDI-2015-LopesMNR #optimisation

Provably correct peephole optimizations with alive (NPL, DM, SN, JR), pp. 22–32.

PLDI-2015-FaddegonC #algorithm #debugging #dependence #haskell #source code #stack

Algorithmic debugging of real-world haskell programs: deriving dependencies from the cost centre stack (MF, OC), pp. 33–42.

PLDI-2015-Sidiroglou-Douskos #automation #fault #multi

Automatic error elimination by horizontal code transfer across multiple applications (SSD, EL, FL, MR), pp. 43–54.

PLDI-2015-0010ZTZ #bound #named

Light: replay via tightly bounded recording (PL, XZ, OT, YZ), pp. 55–64.

PLDI-2015-LidburyLCD #compilation #fuzzing #manycore

Many-core compiler fuzzing (CL, AL, NC, AFD), pp. 65–76.

PLDI-2015-SergeyNB #concurrent #fine-grained #source code #verification

Mechanized verification of fine-grained concurrent programs (IS, AN, AB), pp. 77–87.

PLDI-2015-SharmaBA #gpu #source code #verification

Verification of producer-consumer synchronization in GPU programs (RS, MB, AA), pp. 88–98.

PLDI-2015-GammieHE #garbage collection #on the fly

Relaxing safely: verified on-the-fly garbage collection for x86-TSO (PG, ALH, KE), pp. 99–109.

PLDI-2015-TassarottiDV #logic #memory management #verification

Verifying read-copy-update in a logic for weak memory (JT, DD, VV), pp. 110–120.

PLDI-2015-KoBS #named

LaminarIR: compile-time queues for structured streams (YK, BB, BS), pp. 121–130.

PLDI-2015-DingTKZK #multi #optimisation

Optimizing off-chip accesses in multicores (WD, XT, MTK, YZ, EK), pp. 131–142.

PLDI-2015-MehtaY #compilation #optimisation #scalability #source code

Improving compiler scalability: optimizing large programs at small price (SM, PCY), pp. 143–152.

PLDI-2015-Appel #encryption #verification

Verification of a cryptographic primitive: SHA-256 (AWA), p. 153.

PLDI-2015-DeligiannisDKLT #analysis #programming #state machine #testing

Asynchronous programming, analysis and testing with state machines (PD, AFD, JK, AL, PT), pp. 154–164.

PLDI-2015-Huang #concurrent #model checking #reduction #source code

Stateless model checking concurrent programs with maximal causality reduction (JH), pp. 165–174.

PLDI-2015-SamakRJ #testing

Synthesizing racy tests (MS, MKR, SJ), pp. 175–185.

PLDI-2015-KoskinenP #transaction

The Push/Pull model of transactions (EK, MJP), pp. 186–195.

PLDI-2015-McClurgHCF #network #performance #synthesis

Efficient synthesis of network updates (JM, HH, PC, NF), pp. 196–207.

PLDI-2015-NoriORV #performance #probability #source code #synthesis

Efficient synthesis of probabilistic programs (AVN, SO, SKR, DV), pp. 208–217.

PLDI-2015-BarowyGHZ #named #relational #spreadsheet #using

FlashRelate: extracting relational data from semi-structured spreadsheets using examples (DWB, SG, TH, BGZ), pp. 218–228.

PLDI-2015-FeserCD #data type

Synthesizing data structure transformations from input-output examples (JKF, SC, ID), pp. 229–239.

PLDI-2015-ZivAGRS #concurrent

Composing concurrency control (OZ, AA, GGG, GR, MS), pp. 240–249.

PLDI-2015-ZhangKW #memory management #modelling #partial order #reduction

Dynamic partial order reduction for relaxed memory models (NZ, MK, CW), pp. 250–259.

PLDI-2015-EmmiEH #monitoring #reasoning #refinement

Monitoring refinement via symbolic reasoning (ME, CE, JH), pp. 260–269.

PLDI-2015-LongfieldNMT #self #specification

Preventing glitches and short circuits in high-level self-timed chip specifications (SLJ, BN, RM, RT), pp. 270–279.

PLDI-2015-LalQ #graph #source code

DAG inlining: a decision procedure for reachability-modulo-theories in hierarchical programs (AL, SQ), pp. 280–290.

PLDI-2015-JohnsonWMC #dependence #graph #security

Exploring and enforcing security guarantees via program dependence graphs (AJ, LW, SM, SC), pp. 291–302.

PLDI-2015-SinghPV #performance #program analysis

Making numerical program analysis fast (GS, MP, MTV), pp. 303–313.

PLDI-2015-WeijiangBLK #analysis #dependence

Tree dependence analysis (YW, SB, JL, MK), pp. 314–325.

PLDI-2015-KangHMGZV #c #memory management

A formal C memory model supporting integer-pointer casts (JK, CKH, WM, DG, SZ, VV), pp. 326–335.

PLDI-2015-HathhornER #c

Defining the undefinedness of C (CH, CE, GR), pp. 336–345.

PLDI-2015-ParkSR #javascript #named #semantics

KJS: a complete formal semantics of JavaScript (DP, AS, GR), pp. 346–356.

PLDI-2015-WilcoxWPTWEA #distributed #framework #implementation #named #verification

Verdi: a framework for implementing and formally verifying distributed systems (JRW, DW, PP, ZT, XW, MDE, TEA), pp. 357–368.

PLDI-2015-OlivoDL #debugging #detection #performance #static analysis #traversal

Static detection of asymptotic performance bugs in collection traversals (OO, ID, CL), pp. 369–378.

PLDI-2015-DingAVSOA #algorithm

Autotuning algorithmic choice for input sensitivity (YD, JA, KV, XS, UMO, SPA), pp. 379–390.

PLDI-2015-MendisBWKRPZA #domain-specific language #kernel #named

Helium: lifting high-performance stencil kernels from stripped x86 binaries to halide DSL code (CM, JB, KW, SK, JRK, SP, QZ, SPA), pp. 391–402.

PLDI-2015-BowmanMSD #metaprogramming

Profile-guided meta-programming (WJB, SM, VSA, RKD), pp. 403–412.

PLDI-2015-Sivaramakrishnan #consistency #declarative #programming

Declarative programming over eventually consistent data stores (KCS, GK, SJ), pp. 413–424.

PLDI-2015-SiekTW

Blame and coercion: together again for the first time (JGS, PT, PW), pp. 425–435.

PLDI-2015-ZhangLSLM #flexibility #lightweight #object-oriented

Lightweight, flexible object-oriented generics (YZ, MCL, GS, BL, ACM), pp. 436–445.

PLDI-2015-NguyenH #higher-order #source code

Relatively complete counterexamples for higher-order programs (PCN, DVH), pp. 446–456.

PLDI-2015-ChuJT #automation #imperative #induction #proving #source code

Automatic induction proofs of data-structures in imperative programs (DHC, JJ, MTT), pp. 457–466.

PLDI-2015-Carbonneaux0S #bound #composition

Compositional certified resource bounds (QC, JH, ZS), pp. 467–478.

PLDI-2015-CraryS #peer-to-peer #using

Peer-to-peer affine commitment using bitcoin (KC, MJS), pp. 479–488.

PLDI-2015-LeQC #specification #termination

Termination and non-termination specification inference (TCL, SQ, WNC), pp. 489–498.

PLDI-2015-EmaniO #approach #runtime

Celebrating diversity: a mixture of experts approach for runtime mapping in dynamic environments (MKE, MFPO), pp. 499–508.

PLDI-2015-RenJKAK #execution #hardware #performance #recursion #source code

Efficient execution of recursive programs on commodity vector hardware (BR, YJ, SK, KA, MK), pp. 509–520.

PLDI-2015-VenkatHS #data transformation #matrix

Loop and data transformations for sparse matrix code (AV, MWH, MS), pp. 521–532.

PLDI-2015-PrountzosMP #automation #graph #parallel #source code

Synthesizing parallel graph programs via automated planning (DP, RM, KP), pp. 533–544.

PLDI-2015-MarrSD #metaprogramming #performance #protocol

Zero-overhead metaprogramming: reflection and metaobject protocols fast and without compromises (SM, CS, SD), pp. 545–554.

PLDI-2015-IsradisaikulM #parsing

Finding counterexamples from parsing conflicts (CI, ACM), pp. 555–564.

PLDI-2015-LeungSL #interactive #parsing #synthesis

Interactive parser synthesis by example (AL, JS, SL), pp. 565–574.

PLDI-2015-LuciaR #execution #programming

A simpler, safer programming and execution model for intermittent systems (BL, BR), pp. 575–585.

PLDI-2015-MachadoLR #concurrent #debugging #difference

Concurrency debugging with differential schedule projections (NM, BL, LETR), pp. 586–595.

PLDI-2015-SrinivasanR #semantics #synthesis

Synthesis of machine code from semantics (VS, TWR), pp. 596–607.

PLDI-2015-GonnordMR #ranking #synthesis #using

Synthesis of ranking functions using extremal counterexamples (LG, DM, GR), pp. 608–618.

PLDI-2015-OseraZ #synthesis

Type-and-example-directed program synthesis (PMO, SZ), pp. 619–630.