Venues / PLDI /

PLDI 2022

68 papers

"Synthesizing input grammars": a replication study · Bachir Bendrissou, Rahul Gopinath, Andreas Zeller
A flexible type system for fearless concurrency · Mae Milano, Joshua Turcotti, Andrew C. Myers
A study of real-world data races in Golang · Milind Chabbi, Murali Krishna Ramanathan
A typed continuation-passing translation for lexical effect handlers · Philipp Schuster, Jonathan Immanuel Brachthäuser, Marius Müller, Klaus Ostermann
ANOSY: approximated knowledge synthesis with refinement types for declassification · Sankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker
Abstract interpretation repair · Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Francesco Ranzato
Adore: atomic distributed objects with certified reconfiguration · Wolf Honoré, Ji-Yong Shin, Jieung Kim, Zhong Shao
Algebraic reasoning of Quantum programs via non-idempotent Kleene algebra · Yuxiang Peng, Mingsheng Ying, Xiaodi Wu
All you need is superword-level parallelism: systematic control-flow vectorization with SLP · Yishen Chen, Charith Mendis, Saman P. Amarasinghe
Autoscheduling for sparse tensor algebra with an asymptotic cost model · Willow Ahrens, Fredrik Kjolstad, Saman P. Amarasinghe
Bind the gap: compiling real software to hardware FFT accelerators · Jackson Woodruff, Jordi Armengol-Estapé, Sam Ainsworth, Michael F. P. O'Boyle
Can reactive synthesis and syntax-guided synthesis be friends? · Wonhyuk Choi, Bernd Finkbeiner, Ruzica Piskac, Mark Santolucito
Certified mergeable replicated data types · Vimala Soundarapandian, Adharsh Kamath, Kartik Nagar, K. C. Sivaramakrishnan
Checking robustness to weak persistency models · Hamed Gorjiara, Weiyu Luo, Alex Lee, Guoqing Harry Xu, Brian Demsky
Choosing mathematical function implementations for speed and accuracy · Ian Briggs, Pavel Panchekha
Compass: strong and compositional library specifications in relaxed memory separation logic · Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang + 1 more
Computing correctly with inductive relations · Zoe Paraskevopoulou, Aaron Eline, Leonidas Lampropoulos
CycleQ: an efficient basis for cyclic equational reasoning · Eddie Jones, C.-H. Luke Ong, Steven J. Ramsay
DISTAL: the distributed tensor algebra compiler · Rohan Yadav, Alex Aiken, Fredrik Kjolstad
Deep and shallow types for gradual languages · Ben Greenman
Deoptless: speculation with dispatched on-stack replacement and specialized continuations · Olivier Flückiger, Jan Jecmen, Sebastián Krynski, Jan Vitek
Diaframe: automated verification of fine-grained concurrent programs in Iris · Ike Mulder, Robbert Krebbers, Herman Geuvers
Differential cost analysis with simultaneous potentials and anti-potentials · Dorde Zikelic, Bor-Yuh Evan Chang, Pauline Bolignano, Franco Raimondi
Efficient approximations for cache-conscious data placement · Ali Ahmadi, Majid Daliri, Amir Kafshdar Goharshady, Andreas Pavlogiannis
Exocompilation for productive programming of hardware accelerators · Yuka Ikarashi, Gilbert Louis Bernstein, Alex Reinking, Hasan Genc, Jonathan Ragan-Kelley
Finding the dwarf: recovering precise types from WebAssembly binaries · Daniel Lehmann, Michael Pradel
Finding typing compiler bugs · Stefanos Chaliasos, Thodoris Sotiropoulos, Diomidis Spinellis, Arthur Gervais, Benjamin Livshits, Dimitris Mitropoulos
Formally verified lifting of C-compiled x86-64 binaries · Freek Verbeek, Joshua A. Bockenek, Zhoulai Fu, Binoy Ravindran
FreeTensor: a free-form DSL with holistic optimizations for irregular tensor programs · Shizhi Tang, Jidong Zhai, Haojie Wang, Lin Jiang, Liyan Zheng, Zhenhao Yuan + 1 more
Giallar: push-button verification for the qiskit Quantum compiler · Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross + 2 more
Guaranteed bounds for posterior inference in universal probabilistic programming · Raven Beutner, C.-H. Luke Ong, Fabian Zaiser
Hamband: RDMA replicated data types · Farzin Houshmand, Javad Saberlatibari, Mohsen Lesani
Hardening attack surfaces with formally proven binary format parsers · Nikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy + 4 more
IRDL: an IR definition language for SSA compilers · Mathieu Fehr, Jeff Niu, River Riddle, Mehdi Amini, Zhendong Su, Tobias Grosser
Interpreter-guided differential JIT compiler unit testing · Guillermo Polito, Stéphane Ducasse, Pablo Tesone
Islaris: verification of machine code against authoritative ISA semantics · Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer + 2 more
Karp: a language for NP reductions · Chenhao Zhang, Jason D. Hartline, Christos Dimoulas
Kleene algebra modulo theories: a framework for concrete KATs · Michael Greenberg, Ryan Beckett, Eric Hayden Campbell
Landmarks and regions: a robust approach to data extraction · Suresh Parthasarathy, Lincy Pattanaik, Anirudh Khatry, Arun Iyer, Arjun Radhakrishna, Sriram K. Rajamani + 1 more
Lasagne: a static binary translator for weak memory model architectures · Rodrigo C. O. Rocha, Dennis Sprokholt, Martin Fink, Redha Gouicem, Tom Spink, Soham Chakraborty + 1 more
Leapfrog: certified equivalence for protocol parsers · Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, Greg Morrisett
Low-latency, high-throughput garbage collection · Wenyu Zhao, Stephen M. Blackburn, Kathryn S. McKinley
Mako: a low-pause, high-throughput evacuating collector for memory-disaggregated datacenters · Haoran Ma, Shi Liu, Chenxi Wang, Yifan Qiao, Michael D. Bond, Stephen M. Blackburn + 2 more
Modular information flow through ownership · Will Crichton, Marco Patrignani, Maneesh Agrawala, Pat Hanrahan
Odin: on-demand instrumentation with on-the-fly recompilation · Mingzhe Wang, Jie Liang, Chijin Zhou, Zhiyong Wu, Xinyi Xu, Yu Jiang
P4BID: information flow control in p4 · Karuna Grewal, Loris D'Antoni, Justin Hsu
PDL: a high-level hardware design language for pipelined processors · Drew Zagieboylo, Charles Sherk, Gookwon Edward Suh, Andrew C. Myers
PaC-trees: supporting parallel and compressed purely-functional collections · Laxman Dhulipala, Guy E. Blelloch, Yan Gu, Yihan Sun
Progressive polynomial approximations for fast correctly rounded math libraries · Mridul Aanjaneya, Jay P. Lim, Santosh Nagarakatte
PyLSE: a pulse-transfer level language for superconductor electronics · Michael Christensen, Georgios Tzimpragos, Harlan Kringen, Jennifer Volk, Timothy Sherwood, Ben Hardekopf
Quartz: superoptimization of Quantum circuits · Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth + 5 more
Quickstrom: property-based acceptance testing with LTL specifications · Liam O'Connor, Oskar Wickström
Recursion synthesis with unrealizability witnesses · Azadeh Farzan, Danya Lette, Victor Nicolet
Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code · Clément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala
RunTime-assisted convergence in replicated data types · Gowtham Kaki, Prasanth Prahladan, Nicholas V. Lewchenko
RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code · Yusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer
Semantic soundness for language interoperability · Daniel Patterson, Noble Mushtak, Andrew Wagner, Amal Ahmed
Sequential reasoning for optimizing compilers under weak memory concurrency · Minki Cho, Sung-Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav
Software-hardware codesign for efficient in-memory regular pattern matching · Lingkun Kong, Qixuan Yu, Agnishom Chattopadhyay, Alexis Le Glaunec, Yi Huang, Konstantinos Mamouras + 1 more
Sound sequentialization for concurrent program verification · Azadeh Farzan, Dominik Klumpp, Andreas Podelski
Synthesizing analytical SQL queries from computation demonstration · Xiangyu Zhou, Rastislav Bodík, Alvin Cheung, Chenglong Wang
Turning manual concurrent memory reclamation into automatic reference counting · Daniel Anderson, Guy E. Blelloch, Yuanhao Wei
Type-directed program synthesis for RESTful APIs · Zheng Guo, David Cao, Davin Tjong, Jean Yang, Cole Schlesinger, Nadia Polikarpova
Verifying optimizations of concurrent programs in the promising semantics · Junpeng Zha, Hongjin Liang, Xinyu Feng
Visualization question answering using introspective program synthesis · Yanju Chen, Xifeng Yan, Yu Feng
WARio: efficient code generation for intermittent computing · Vito Kortbeek, Souradip Ghosh, Josiah D. Hester, Simone Campanoni, Przemyslaw Pawelczak
Warping cache simulation of polyhedral programs · Canberk Morelli, Jan Reineke
WebRobot: web robotic process automation using interactive programming-by-demonstration · Rui Dong, Zhicheng Huang, Ian Iong Lam, Yan Chen, Xinyu Wang