Powered by
43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2022),
June 13–17, 2022,
San Diego, CA, USA
Frontmatter
Security
Hardening Attack Surfaces with Formally Proven Binary Format Parsers
Nikhil Swamy,
Tahina Ramananandro,
Aseem Rastogi, Irina Spiridonova,
Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, and Arti Gupta
(Microsoft Research, USA; Microsoft Research, India; Cornell University, USA; Microsoft, USA)
Publisher's Version
Memory
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,
Miryung Kim, and
Guoqing Harry Xu
(University of California at Los Angeles, USA; Ohio State University, USA; Australian National University, Australia)
Publisher's Version
Synthesis I
Compilation
IRDL: An IR Definition Language for SSA Compilers
Mathieu Fehr, Jeff Niu, River Riddle,
Mehdi Amini,
Zhendong Su, and
Tobias Grosser
(University of Edinburgh, UK; University of Waterloo, Canada; Modular AI, USA; Google, USA; ETH Zurich, Switzerland)
Publisher's Version
Artifacts Reusable
Synthesis II
Tensors
Distribution
Analysis
Concurrency
Numbers
Semantics
Quantum
Quartz: Superoptimization of Quantum Circuits
Mingkuan Xu,
Zikun Li,
Oded Padon, Sina Lin,
Jessica Pointing,
Auguste Hirth,
Henry Ma,
Jens Palsberg,
Alex Aiken,
Umut A. Acar, and
Zhihao Jia
(Carnegie Mellon University, USA; University of California at Los Angeles, USA; VMware Research, USA; Microsoft, USA; University of Oxford, UK; Stanford University, USA)
Publisher's Version
Artifacts Functional
Giallar: Push-Button Verification for the Qiskit Quantum Compiler
Runzhou Tao, Yunong Shi,
Jianan Yao, Xupeng Li,
Ali Javadi-Abhari,
Andrew W. Cross,
Frederic T. Chong, and
Ronghui Gu
(Columbia University, USA; Amazon, USA; IBM Research, USA; University of Chicago, USA)
Publisher's Version
Artifacts Reusable
Hardware
DSLs
Verification I
Islaris: Verification of Machine Code Against Authoritative ISA Semantics
Michael Sammler,
Angus Hammond,
Rodolphe Lepigre,
Brian Campbell,
Jean Pichon-Pharabod,
Derek Dreyer,
Deepak Garg, and
Peter Sewell
(MPI-SWS, Germany; University of Cambridge, UK; University of Edinburgh, UK; Aarhus University, Denmark)
Publisher's Version
Artifacts Reusable
RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code
Yusuke Matsushita,
Xavier Denis,
Jacques-Henri Jourdan, and
Derek Dreyer
(University of Tokyo, Japan; Université Paris-Saclay, France; CNRS, France; ENS Paris-Saclay, France; Inria, France; Laboratoire Méthodes Formelles, France; MPI-SWS, Germany)
Publisher's Version
Artifacts Reusable
Verification and Optimization
Lasagne: A Static Binary Translator for Weak Memory Model Architectures
Rodrigo C. O. Rocha,
Dennis Sprokholt, Martin Fink,
Redha Gouicem,
Tom Spink,
Soham Chakraborty, and
Pramod Bhatotia
(University of Edinburgh, UK; Delft University of Technology, Netherlands; TU Munich, Germany; University of St. Andrews, UK)
Publisher's Version
Archive submitted (930 kB)
Artifacts Reusable
Verification II
Testing and Synthesis
proc time: 8.43