Kathryn S. McKinley, Kathleen Fisher
Proceedings of the 40th Conference on Programming Language Design and Implementation
PLDI, 2019.

@proceedings{PLDI-2019,
	doi           = "10.1145/3314221",
	editor        = "Kathryn S. McKinley and Kathleen Fisher",
	isbn          = "978-1-4503-6712-7",
	publisher     = "{ACM}",
	title         = "{Proceedings of the 40th Conference on Programming Language Design and Implementation}",
	year          = 2019,
}

Contents (76 items)

PLDI-2019-PultePKLH #concurrent #named #performance

Promising-ARM/RISC-V: a simpler and faster operational concurrency model (CP, JPP, JK, SHL, CKH), pp. 1–15.

PLDI-2019-LiuMM #compilation #consistency #java

Accelerating sequential consistency for Java with speculative compilation (LL, TDM, MM), pp. 16–30.

PLDI-2019-ProkopecRLD0SBZ #benchmark #metric #named #parallel #virtual machine

Renaissance: benchmarking suite for parallel applications on the JVM (AP, AR, DL, GD, PT0, MS, LB, YZ, AV, DS, TW, WB), pp. 31–47.

PLDI-2019-VollmerKRS0N #named #source code

LoCal: a language for programs operating on serialized data (MV0, CK, MR, LS, MK0, RRN), pp. 48–62.

PLDI-2019-FremontDGYSS #generative #named #specification

Scenic: a language for scenario specification and scene generation (DJF, TD, SG, XY, ALSV, SAS), pp. 63–78.

PLDI-2019-GopinathGSS #compilation #machine learning #modelling

Compiling KB-sized machine learning models to tiny IoT devices (SG, NG, VS, RS0), pp. 79–95.

PLDI-2019-Kokologiannakis #consistency #library #model checking

Model checking for weakly consistent libraries (MK, AR, VV), pp. 96–110.

PLDI-2019-JiangLXZF #compilation #concurrent #source code #towards

Towards certified separate compilation for concurrent programs (HJ, HL, SX, JZ, XF), pp. 111–125.

PLDI-2019-LahavM #robust #semantics

Robustness against release/acquire semantics (OL, RM), pp. 126–141.

PLDI-2019-DathathriS0LLMM #compilation #named #optimisation

CHET: an optimizing compiler for fully-homomorphic neural-network inferencing (RD, OS, HC0, KL, KEL, SM, MM, TM), pp. 142–156.

PLDI-2019-MercadierD #named

Usuba: high-throughput and constant-time ciphers, by construction (DM, PÉD), pp. 157–173.

PLDI-2019-CauligiSJBWRGBJ #domain-specific language #named

FaCT: a DSL for timing-sensitive computation (SC, GS, BJ, FB, RSW, JR, BG, GB, RJ, DS), pp. 174–189.

PLDI-2019-SmolkaKKFHK0 #network #probability #scalability #verification

Scalable verification of probabilistic networks (SS, PK0, DMK, NF, JH, DK, AS0), pp. 190–203.

PLDI-2019-Wang0GCQS #cost analysis #nondeterminism #probability #source code

Cost analysis of nondeterministic probabilistic programs (PW, HF0, AKG, KC, XQ, WS), pp. 204–220.

PLDI-2019-Cusumano-Towner #named #probability #programmable #programming

Gen: a general-purpose probabilistic programming system with programmable inference (MFCT, FAS, AKL, VKM), pp. 221–236.

PLDI-2019-ZhangX #incremental #probability #source code

Incremental precision-preserving symbolic inference for probabilistic programs (JZ, JX), pp. 237–252.

PLDI-2019-KnothWP0 #synthesis

Resource-guided program synthesis (TK, DW, NP, JH0), pp. 253–268.

PLDI-2019-0001R #database #learning #modelling #using

Using active learning to synthesize models of applications that access databases (JS0, MCR), pp. 269–285.

PLDI-2019-0001DSD #database #refactoring #source code

Synthesizing database programs for schema refactoring (YW0, JD, RS, ID), pp. 286–300.

PLDI-2019-IyerJPRR #machine learning #synthesis

Synthesis and machine learning for heterogeneous extraction (ASI, MJ, SP, AR, SKR), pp. 301–315.

PLDI-2019-ShullHT #framework #java #named #reachability

AutoPersist: an easy-to-use Java NVM framework based on reachability (TS, JH0, JT), pp. 316–332.

PLDI-2019-PowersTB0 #c #c++ #memory management #named

Mesh: compacting memory management for C/C++ applications (BP, DT, EDB, AM0), pp. 333–346.

PLDI-2019-WangCCZVML0X #big data #hybrid #memory management #named

Panthera: holistic memory management for big data processing over hybrid memories (CW, HC, TC, JZ, HV0, OM, FL, XF0, GHX), pp. 347–362.

PLDI-2019-TonderG #combinator #lightweight #multi #parsing #syntax

Lightweight multi-language syntax transformation with parser parser combinators (RvT, CLG), pp. 363–378.

PLDI-2019-KrishnaswamiY #algebra #approach #parsing

A typed, algebraic approach to parsing (NRK, JY), pp. 379–393.

PLDI-2019-CampagnaXMSL #generative #named #natural language #parsing #semantics

Genie: a generator of natural language semantic parsers for virtual assistant commands (GC, SX, MM, RS, MSL), pp. 394–410.

PLDI-2019-HallahanXBJP #execution #lazy evaluation #symbolic computation

Lazy counterfactual symbolic execution (WTH, AX, MTB, RJ, RP), pp. 411–424.

PLDI-2019-LoringMK #execution #javascript #regular expression #semantics #symbolic computation

Sound regular expression semantics for dynamic symbolic execution of JavaScript (BL, DM, JK), pp. 425–438.

PLDI-2019-FuS #analysis #effectiveness #float

Effective floating-point analysis via weak-distance minimization (ZF, ZS), pp. 439–452.

PLDI-2019-KhanZPMK #detection #hybrid #named

Huron: hybrid false sharing detection and repair (TAK, YZ, GP, BM, BK), pp. 453–468.

PLDI-2019-KongP #manycore #modelling

Model-driven transformations for multi- and many-core CPUs (MK, LNP), pp. 469–484.

PLDI-2019-YogaN #analysis #difference

Parallelism-centric what-if and differential analyses (AY, SN), pp. 485–501.

PLDI-2019-ScalasYB #behaviour #message passing #source code #verification

Verifying message-passing programs with dependent behavioural types (AS, NY, EB), pp. 502–516.

PLDI-2019-KuhlenschmidtAS #performance #towards #type system

Toward efficient gradual typing for structural types via coercions (AK, DA, JGS), pp. 517–532.

PLDI-2019-CicekQBG0 #bidirectional #relational #type checking

Bidirectional type checking for relational properties (EÇ, WQ, GB, MG, DG0), pp. 533–547.

PLDI-2019-MathisGMKHZ #fuzzing

Parser-directed fuzzing (BM, RG, MM, AK, MH, AZ), pp. 548–560.

PLDI-2019-HeoRSN #difference #reasoning #source code #using

Continuously reasoning about programs using differential Bayesian inference (KH, MR, XS, MN), pp. 561–575.

PLDI-2019-LidburyD #scheduling

Sparse record and replay with controlled scheduling (CL, AFD), pp. 576–593.

PLDI-2019-MohammadiYCDHDN #data flow #dependence #performance

Sparse computation data dependence simplification for efficient compiler-generated inspectors (MSM, TY, KC, ECD, MWH, MMD, PN, CO, AV, MMS), pp. 594–609.

PLDI-2019-FarzanN #composition #divide and conquer #parallel

Modular divide-and-conquer parallelization of nested loops (AF, VN), pp. 610–624.

PLDI-2019-AugustineSP0 #generative

Generating piecewise-regular code from irregular structures (TA, JS, LNP, GR0), pp. 625–639.

PLDI-2019-LiaoHM #calculus #composition #encryption #named

ILC: a calculus for composable, computational cryptography (KL, MAH, AM0), pp. 640–654.

PLDI-2019-WangDWKZ #difference #execution #privacy #proving

Proving differential privacy with shadow execution (YW, ZD, GW, DK, DZ), pp. 655–669.

PLDI-2019-MamourasSAIT #distributed

Data-trace types for distributed stream processing systems (KM, CS, RA, ZGI, VT), pp. 670–685.

PLDI-2019-ZhuXMJ #framework #induction #learning #synthesis

An inductive synthesis framework for verifiable reinforcement learning (HZ0, ZX, SM, SJ), pp. 686–701.

PLDI-2019-LeeLLMZ #programming

Programming support for autonomizing software (WCL, PL, YL, SM, XZ), pp. 702–716.

PLDI-2019-GuanSL #framework #named #performance

Wootz: a compiler-based framework for fast CNN pruning via composability (HG, XS, SHL), pp. 717–730.

PLDI-2019-AndersonPDC #abstraction #approach #network #optimisation #robust

Optimization and abstraction: a synergistic approach for analyzing neural network robustness (GA, SP, ID, SC), pp. 731–744.

PLDI-2019-EberhardtSRV #alias #api #learning #specification

Unsupervised learning of API aliasing specifications (JE, SS, VR, MTV), pp. 745–759.

PLDI-2019-ChibotaruBRV #scalability #specification

Scalable taint specification inference with big code (VC, BB, VR, MTV), pp. 760–774.

PLDI-2019-AstorgaMSWX #generative #learning

Learning stateful preconditions modulo a test generator (AA, PM, SS, SW, TX0), pp. 775–787.

PLDI-2019-LeZN #dynamic analysis #invariant #logic #named #using

SLING: using dynamic analysis to infer program invariants in separation logic (TCL, GZ, TN), pp. 788–801.

PLDI-2019-Wu0 #abstract interpretation #execution

Abstract interpretation under speculative execution (MW, CW0), pp. 802–815.

PLDI-2019-GysiGBH #performance

A fast analytical model of fully associative caches (TG, TG, LB, TH), pp. 816–829.

PLDI-2019-SakkaSN0 #fine-grained #traversal

Sound, fine-grained traversal fusion for heterogeneous trees (LS, KS, RRN, MK0), pp. 830–844.

PLDI-2019-NguyenGTH #contract #higher-order #source code #termination

Size-change termination as a contract: dynamically and statically enforcing termination for higher-order programs (PCN, TG, STH, DVH), pp. 845–859.

PLDI-2019-PerryKSZ #clustering #imperative #named #programming #semantics

SemCluster: clustering of imperative programming assignments based on quantitative semantic features (DMP, DK, RS, XZ), pp. 860–873.

PLDI-2019-KapusIIRC #c #refactoring #string #summary #testing

Computing summaries of string loops in C for better testing and refactoring (TK, OIS, SI, NR, CC), pp. 874–888.

PLDI-2019-ChoiST #javascript #performance #reuse

Reusable inline caching for JavaScript performance (JC, TS, JT), pp. 889–901.

PLDI-2019-Sundararajah0 #composition #recursion

Composable, sound transformations of nested recursion and loops (KS, MK0), pp. 902–917.

PLDI-2019-DhulipalaBS #graph #streaming #using

Low-latency graph streaming using compressed purely-functional trees (LD, GEB, JS), pp. 918–934.

PLDI-2019-TangKKA #parallel

Co-optimizing memory-level parallelism and cache-level parallelism (XT, MTK, MK, MA), pp. 935–949.

PLDI-2019-RoweFTO #implementation #ml

Characterising renaming within OCaml's module system: theory and implementation (RNSR, HF, SJT, SO), pp. 950–965.

PLDI-2019-KazerounianGVFH #library #ruby

Type-level computations for Ruby libraries (MK, SNG, NV, JSF, DVH), pp. 966–979.

PLDI-2019-WangEMP

Replication-aware linearizability (CW, CE, SOM, GP), pp. 980–993.

PLDI-2019-LiLCGL #automation #debugging #distributed #named

DFix: automatically fixing timing bugs in distributed systems (GL, HL, XC, HSG, SL), pp. 994–1009.

PLDI-2019-VasilakisKPSDS #named #scalability

Ignis: scaling distribution-oblivious systems with light-touch distribution (NV, BK, YP, JS, AD, JMS), pp. 1010–1026.

PLDI-2019-ChurchillP0A #equivalence #semantics

Semantic program alignment for equivalence checking (BRC, OP, RS0, AA), pp. 1027–1040.

PLDI-2019-LoowKTMNAF #compilation

Verified compilation on a verified processor (AL, RK, YKT, MOM, MN, OA, ACJF), pp. 1041–1053.

PLDI-2019-ChajedTKZ #named #refinement #verification

Argosy: verifying layered storage systems with recovery refinement (TC, JT, MFK, NZ), pp. 1054–1068.

PLDI-2019-GershuniAGNNRRS #kernel #linux #precise #static analysis

Simple and precise static analysis of untrusted Linux kernel extensions (EG, NA, AG, NN, JAN, NR, LR, MS), pp. 1069–1084.

PLDI-2019-RuppelL #concurrent #energy #transaction

Transactional concurrency control for intermittent, energy-harvesting computing systems (ER, BL), pp. 1085–1100.

PLDI-2019-MaengL

Supporting peripherals in intermittent systems with just-in-time checkpoints (KM, BL), pp. 1101–1116.

PLDI-2019-AbdullaAAK #semantics #source code #verification

Verification of programs under the release-acquire semantics (PAA, JA0, MFA, SNK), pp. 1117–1132.

PLDI-2019-Dasgupta0KAR #architecture #semantics #set

A complete formal semantics of x86-64 user-level instruction set architecture (SD, DP0, TK, VSA, GR), pp. 1133–1148.

PLDI-2019-ZhouYY #hoare #logic #quantum

An applied quantum Hoare logic (LZ, NY, MY), pp. 1149–1162.