![](https://dblp.uni-trier.de./img/logo.320x120.png)
![search dblp search dblp](https://dblp.uni-trier.de./img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de./img/search.dark.16x16.png)
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
![](https://dblp.uni-trier.de./img/cog.dark.24x24.png)
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.