


default search action
PLDI 2022: San Diego, CA, USA
- Ranjit Jhala, Isil Dillig:

PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022. ACM 2022, ISBN 978-1-4503-9265-5
Security
- Will Crichton

, Marco Patrignani
, Maneesh Agrawala
, Pat Hanrahan:
Modular information flow through ownership. 1-14 - Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker:

ANOSY: approximated knowledge synthesis with refinement types for declassification. 15-30 - Nikhil Swamy, Tahina Ramananandro

, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, Arti Gupta:
Hardening attack surfaces with formally proven binary format parsers. 31-45 - Karuna Grewal, Loris D'Antoni, Justin Hsu:

P4BID: information flow control in p4. 46-60
Memory
- Daniel Anderson, Guy E. Blelloch, Yuanhao Wei:

Turning manual concurrent memory reclamation into automatic reference counting. 61-75 - Wenyu Zhao, Stephen M. Blackburn, Kathryn S. McKinley:

Low-latency, high-throughput garbage collection. 76-91 - Haoran Ma, Shi Liu, Chenxi Wang

, Yifan Qiao, Michael D. Bond
, Stephen M. Blackburn, Miryung Kim, Guoqing Harry Xu
:
Mako: a low-pause, high-throughput evacuating collector for memory-disaggregated datacenters. 92-107 - Laxman Dhulipala, Guy E. Blelloch, Yan Gu, Yihan Sun

:
PaC-trees: supporting parallel and compressed purely-functional collections. 108-121
Synthesis I
- Zheng Guo, David Cao

, Davin Tjong, Jean Yang, Cole Schlesinger, Nadia Polikarpova:
Type-directed program synthesis for RESTful APIs. 122-136 - Yanju Chen

, Xifeng Yan, Yu Feng
:
Visualization question answering using introspective program synthesis. 137-151 - Rui Dong

, Zhicheng Huang, Ian Iong Lam, Yan Chen
, Xinyu Wang
:
WebRobot: web robotic process automation using interactive programming-by-demonstration. 152-167 - Xiangyu Zhou, Rastislav Bodík, Alvin Cheung

, Chenglong Wang:
Synthesizing analytical SQL queries from computation demonstration. 168-182
Compilation
- Stefanos Chaliasos, Thodoris Sotiropoulos, Diomidis Spinellis

, Arthur Gervais, Benjamin Livshits, Dimitris Mitropoulos:
Finding typing compiler bugs. 183-198 - Mathieu Fehr, Jeff Niu, River Riddle, Mehdi Amini, Zhendong Su, Tobias Grosser

:
IRDL: an IR definition language for SSA compilers. 199-212 - Minki Cho

, Sung-Hwan Lee
, Dongjae Lee
, Chung-Kil Hur
, Ori Lahav
:
Sequential reasoning for optimizing compilers under weak memory concurrency. 213-228
Synthesis II
- Wonhyuk Choi, Bernd Finkbeiner, Ruzica Piskac, Mark Santolucito

:
Can reactive synthesis and syntax-guided synthesis be friends? 229-243 - Azadeh Farzan, Danya Lette, Victor Nicolet

:
Recursion synthesis with unrealizability witnesses. 244-259 - Bachir Bendrissou

, Rahul Gopinath
, Andreas Zeller:
"Synthesizing input grammars": a replication study. 260-268
Tensors
- Willow Ahrens

, Fredrik Kjolstad
, Saman P. Amarasinghe:
Autoscheduling for sparse tensor algebra with an asymptotic cost model. 269-285 - Rohan Yadav

, Alex Aiken
, Fredrik Kjolstad
:
DISTAL: the distributed tensor algebra compiler. 286-300 - Yishen Chen, Charith Mendis

, Saman P. Amarasinghe:
All you need is superword-level parallelism: systematic control-flow vectorization with SLP. 301-315 - Canberk Morelli, Jan Reineke:

Warping cache simulation of polyhedral programs. 316-331
Distribution
- Vimala Soundarapandian, Adharsh Kamath

, Kartik Nagar, K. C. Sivaramakrishnan:
Certified mergeable replicated data types. 332-347 - Farzin Houshmand, Javad Saberlatibari, Mohsen Lesani

:
Hamband: RDMA replicated data types. 348-363 - Gowtham Kaki

, Prasanth Prahladan, Nicholas V. Lewchenko:
RunTime-assisted convergence in replicated data types. 364-378 - Wolf Honoré, Ji-Yong Shin

, Jieung Kim, Zhong Shao
:
Adore: atomic distributed objects with certified reconfiguration. 379-394
Analysis
- Eddie Jones

, C.-H. Luke Ong, Steven J. Ramsay
:
CycleQ: an efficient basis for cyclic equational reasoning. 395-409 - Daniel Lehmann, Michael Pradel:

Finding the dwarf: recovering precise types from WebAssembly binaries. 410-425 - Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Francesco Ranzato:

Abstract interpretation repair. 426-441 - Dorde Zikelic, Bor-Yuh Evan Chang, Pauline Bolignano, Franco Raimondi

:
Differential cost analysis with simultaneous potentials and anti-potentials. 442-457
Concurrency
- Mae Milano

, Joshua Turcotti, Andrew C. Myers:
A flexible type system for fearless concurrency. 458-473 - Milind Chabbi, Murali Krishna Ramanathan:

A study of real-world data races in Golang. 474-489 - Hamed Gorjiara, Weiyu Luo, Alex Lee, Guoqing Harry Xu

, Brian Demsky:
Checking robustness to weak persistency models. 490-505 - Azadeh Farzan, Dominik Klumpp

, Andreas Podelski:
Sound sequentialization for concurrent program verification. 506-521
Numbers
- Ian Briggs, Pavel Panchekha

:
Choosing mathematical function implementations for speed and accuracy. 522-535 - Raven Beutner, C.-H. Luke Ong, Fabian Zaiser

:
Guaranteed bounds for posterior inference in universal probabilistic programming. 536-551 - Mridul Aanjaneya

, Jay P. Lim
, Santosh Nagarakatte:
Progressive polynomial approximations for fast correctly rounded math libraries. 552-565
Semantics
- Philipp Schuster, Jonathan Immanuel Brachthäuser

, Marius Müller
, Klaus Ostermann:
A typed continuation-passing translation for lexical effect handlers. 566-579 - Ben Greenman

:
Deep and shallow types for gradual languages. 580-593 - Michael Greenberg

, Ryan Beckett, Eric Hayden Campbell:
Kleene algebra modulo theories: a framework for concrete KATs. 594-608 - Daniel Patterson

, Noble Mushtak, Andrew Wagner
, Amal Ahmed
:
Semantic soundness for language interoperability. 609-624
Quantum
- Mingkuan Xu, Zikun Li, Oded Padon

, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken
, Umut A. Acar, Zhihao Jia:
Quartz: superoptimization of Quantum circuits. 625-640 - Runzhou Tao

, Yunong Shi, Jianan Yao
, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross
, Frederic T. Chong, Ronghui Gu:
Giallar: push-button verification for the qiskit Quantum compiler. 641-656 - Yuxiang Peng, Mingsheng Ying

, Xiaodi Wu:
Algebraic reasoning of Quantum programs via non-idempotent Kleene algebra. 657-670 - Michael Christensen, Georgios Tzimpragos

, Harlan Kringen, Jennifer Volk, Timothy Sherwood
, Ben Hardekopf
:
PyLSE: a pulse-transfer level language for superconductor electronics. 671-686
Hardware
- Jackson Woodruff, Jordi Armengol-Estapé, Sam Ainsworth

, Michael F. P. O'Boyle:
Bind the gap: compiling real software to hardware FFT accelerators. 687-702 - Yuka Ikarashi, Gilbert Louis Bernstein, Alex Reinking

, Hasan Genc, Jonathan Ragan-Kelley:
Exocompilation for productive programming of hardware accelerators. 703-718 - Drew Zagieboylo, Charles Sherk, Gookwon Edward Suh, Andrew C. Myers:

PDL: a high-level hardware design language for pipelined processors. 719-732 - Lingkun Kong, Qixuan Yu, Agnishom Chattopadhyay

, Alexis Le Glaunec, Yi Huang, Konstantinos Mamouras
, Kaiyuan Yang
:
Software-hardware codesign for efficient in-memory regular pattern matching. 733-748
DSLs
- Olivier Flückiger

, Jan Jecmen, Sebastián Krynski, Jan Vitek:
Deoptless: speculation with dispatched on-stack replacement and specialized continuations. 749-761 - Chenhao Zhang, Jason D. Hartline, Christos Dimoulas

:
Karp: a language for NP reductions. 762-776 - Vito Kortbeek, Souradip Ghosh, Josiah D. Hester, Simone Campanoni, Przemyslaw Pawelczak:

WARio: efficient code generation for intermittent computing. 777-791
Verification I
- Hoang-Hai Dang

, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen
, William Mansky, Jeehoon Kang
, Derek Dreyer:
Compass: strong and compositional library specifications in relaxed memory separation logic. 792-808 - Ike Mulder

, Robbert Krebbers, Herman Geuvers:
Diaframe: automated verification of fine-grained concurrent programs in Iris. 809-824 - Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, Peter Sewell

:
Islaris: verification of machine code against authoritative ISA semantics. 825-840 - Yusuke Matsushita

, Xavier Denis
, Jacques-Henri Jourdan, Derek Dreyer:
RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. 841-856
Verification and Optimization
- Ali Ahmadi, Majid Daliri

, Amir Kafshdar Goharshady, Andreas Pavlogiannis
:
Efficient approximations for cache-conscious data placement. 857-871 - Shizhi Tang

, Jidong Zhai, Haojie Wang, Lin Jiang, Liyan Zheng, Zhenhao Yuan, Chen Zhang:
FreeTensor: a free-form DSL with holistic optimizations for irregular tensor programs. 872-887 - Rodrigo C. O. Rocha, Dennis Sprokholt

, Martin Fink
, Redha Gouicem, Tom Spink
, Soham Chakraborty, Pramod Bhatotia:
Lasagne: a static binary translator for weak memory model architectures. 888-902 - Junpeng Zha, Hongjin Liang, Xinyu Feng:

Verifying optimizations of concurrent programs in the promising semantics. 903-917
Verification II
- Clément Pit-Claudel

, Jade Philipoom, Dustin Jamner
, Andres Erbsen, Adam Chlipala:
Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. 918-933 - Freek Verbeek, Joshua A. Bockenek, Zhoulai Fu, Binoy Ravindran:

Formally verified lifting of C-compiled x86-64 binaries. 934-949 - Ryan Doenges, Tobias Kappé

, John Sarracino
, Nate Foster
, Greg Morrisett:
Leapfrog: certified equivalence for protocol parsers. 950-965 - Zoe Paraskevopoulou, Aaron Eline, Leonidas Lampropoulos

:
Computing correctly with inductive relations. 966-980
Testing and Synthesis
- Guillermo Polito, Stéphane Ducasse, Pablo Tesone:

Interpreter-guided differential JIT compiler unit testing. 981-992 - Suresh Parthasarathy, Lincy Pattanaik, Anirudh Khatry

, Arun Iyer, Arjun Radhakrishna
, Sriram K. Rajamani, Mohammad Raza:
Landmarks and regions: a robust approach to data extraction. 993-1009 - Mingzhe Wang, Jie Liang, Chijin Zhou

, Zhiyong Wu, Xinyi Xu, Yu Jiang:
Odin: on-demand instrumentation with on-the-fly recompilation. 1010-1024 - Liam O'Connor

, Oskar Wickström:
Quickstrom: property-based acceptance testing with LTL specifications. 1025-1038

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














