PLDI 2019 – Proceedings

Frontmatter

Concurrency I

Promising-ARM/RISC-V: A Simpler and Faster Operational Concurrency Model
Christopher Pulte, Jean Pichon-Pharabod, Jeehoon Kang, Sung-Hwan Lee, and Chung-Kil Hur
(Cambridge University, UK; KAIST, South Korea; Seoul National University, South Korea)


@InProceedings{PLDI19p1, author = {Christopher Pulte and Jean Pichon-Pharabod and Jeehoon Kang and Sung-Hwan Lee and Chung-Kil Hur}, title = {Promising-ARM/RISC-V: A Simpler and Faster Operational Concurrency Model}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1-0}, doi = {10.1145/3314221.3314624}, year = {2019}, } Publisher's Version Artifacts Functional

Accelerating Sequential Consistency for Java with Speculative Compilation
Lun Liu, Todd Millstein, and Madanlal Musuvathi
(University of California at Los Angeles, USA; Microsoft Research, USA)


@InProceedings{PLDI19p20, author = {Lun Liu and Todd Millstein and Madanlal Musuvathi}, title = {Accelerating Sequential Consistency for Java with Speculative Compilation}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {20-19}, doi = {10.1145/3314221.3314611}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Renaissance: Benchmarking Suite for Parallel Applications on the JVM
Aleksandar Prokopec, Andrea Rosà, David Leopoldseder, Gilles Duboscq, Petr Tůma, Martin Studener, Lubomír Bulej, Yudi Zheng, Alex Villazón, Doug Simon, Thomas Würthinger, and Walter Binder
(Oracle Labs, Switzerland; USI Lugano, Switzerland; JKU Linz, Austria; Charles University in Prague, Czechia; Universidad Privada Boliviana, Bolivia)


@InProceedings{PLDI19p39, author = {Aleksandar Prokopec and Andrea Rosà and David Leopoldseder and Gilles Duboscq and Petr Tůma and Martin Studener and Lubomír Bulej and Yudi Zheng and Alex Villazón and Doug Simon and Thomas Würthinger and Walter Binder}, title = {Renaissance: Benchmarking Suite for Parallel Applications on the JVM}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {39-38}, doi = {10.1145/3314221.3314637}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Language Design I

LoCal: A Language for Programs Operating on Serialized Data
Michael Vollmer, Chaitanya Koparkar, Mike Rainey, Laith Sakka, Milind Kulkarni, and Ryan R. Newton
(Indiana University, USA; Purdue University, USA)


@InProceedings{PLDI19p58, author = {Michael Vollmer and Chaitanya Koparkar and Mike Rainey and Laith Sakka and Milind Kulkarni and Ryan R. Newton}, title = {LoCal: A Language for Programs Operating on Serialized Data}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {58-57}, doi = {10.1145/3314221.3314631}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Scenic: A Language for Scenario Specification and Scene Generation
Daniel J. Fremont, Tommaso Dreossi, Shromona Ghosh, Xiangyu Yue, Alberto L. Sangiovanni-Vincentelli, and Sanjit A. Seshia
(University of California at Berkeley, USA)


@InProceedings{PLDI19p77, author = {Daniel J. Fremont and Tommaso Dreossi and Shromona Ghosh and Xiangyu Yue and Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia}, title = {Scenic: A Language for Scenario Specification and Scene Generation}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {77-76}, doi = {10.1145/3314221.3314633}, year = {2019}, } Publisher's Version

Compiling KB-Sized Machine Learning Models to Tiny IoT Devices
Sridhar Gopinath, Nikhil Ghanathe, Vivek Seshadri, and Rahul Sharma
(Microsoft Research, India)


@InProceedings{PLDI19p96, author = {Sridhar Gopinath and Nikhil Ghanathe and Vivek Seshadri and Rahul Sharma}, title = {Compiling KB-Sized Machine Learning Models to Tiny IoT Devices}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {96-95}, doi = {10.1145/3314221.3314597}, year = {2019}, } Publisher's Version

Concurrency II

Model Checking for Weakly Consistent Libraries
Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis
(MPI-SWS, Germany)


@InProceedings{PLDI19p115, author = {Michalis Kokologiannakis and Azalea Raad and Viktor Vafeiadis}, title = {Model Checking for Weakly Consistent Libraries}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {115-114}, doi = {10.1145/3314221.3314609}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Towards Certified Separate Compilation for Concurrent Programs
Hanru Jiang, Hongjin Liang, Siyang Xiao, Junpeng Zha, and Xinyu Feng
(University of Science and Technology of China, China; Nanjing University, China)


@InProceedings{PLDI19p134, author = {Hanru Jiang and Hongjin Liang and Siyang Xiao and Junpeng Zha and Xinyu Feng}, title = {Towards Certified Separate Compilation for Concurrent Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {134-133}, doi = {10.1145/3314221.3314595}, year = {2019}, } Publisher's Version Artifacts Functional

Robustness against Release/Acquire Semantics
Ori Lahav and Roy Margalit
(Tel Aviv University, Israel)


@InProceedings{PLDI19p153, author = {Ori Lahav and Roy Margalit}, title = {Robustness against Release/Acquire Semantics}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {153-152}, doi = {10.1145/3314221.3314604}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Language Design II

CHET: An Optimizing Compiler for Fully-Homomorphic Neural-Network Inferencing
Roshan Dathathri, Olli Saarikivi, Hao Chen, Kim Laine, Kristin Lauter, Saeed Maleki, Madanlal Musuvathi, and Todd Mytkowicz
(University of Texas at Austin, USA; Microsoft Research, USA)


@InProceedings{PLDI19p172, author = {Roshan Dathathri and Olli Saarikivi and Hao Chen and Kim Laine and Kristin Lauter and Saeed Maleki and Madanlal Musuvathi and Todd Mytkowicz}, title = {CHET: An Optimizing Compiler for Fully-Homomorphic Neural-Network Inferencing}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {172-171}, doi = {10.1145/3314221.3314628}, year = {2019}, } Publisher's Version

Usuba: High-Throughput and Constant-Time Ciphers, by Construction
Darius Mercadier and Pierre-Évariste Dagand
(Sorbonne University, France; CNRS, France; Inria, France; LIP6, France)


@InProceedings{PLDI19p191, author = {Darius Mercadier and Pierre-Évariste Dagand}, title = {Usuba: High-Throughput and Constant-Time Ciphers, by Construction}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {191-190}, doi = {10.1145/3314221.3314636}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

FaCT: A DSL for Timing-Sensitive Computation
Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, and Deian Stefan
(University of California at San Diego, USA; Stanford University, USA; Inria, France; MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain)


@InProceedings{PLDI19p210, author = {Sunjay Cauligi and Gary Soeller and Brian Johannesmeyer and Fraser Brown and Riad S. Wahby and John Renner and Benjamin Grégoire and Gilles Barthe and Ranjit Jhala and Deian Stefan}, title = {FaCT: A DSL for Timing-Sensitive Computation}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {210-209}, doi = {10.1145/3314221.3314605}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Probabilistic Programming

Scalable Verification of Probabilistic Networks
Steffen Smolka, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva
(Cornell University, USA; Carnegie Mellon University, USA; University of Wisconsin-Madison, USA; University College London, UK)


@InProceedings{PLDI19p229, author = {Steffen Smolka and Praveen Kumar and David M. Kahn and Nate Foster and Justin Hsu and Dexter Kozen and Alexandra Silva}, title = {Scalable Verification of Probabilistic Networks}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {229-228}, doi = {10.1145/3314221.3314639}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Cost Analysis of Nondeterministic Probabilistic Programs
Peixin Wang, Hongfei Fu, Amir Kafshdar Goharshady, Krishnendu Chatterjee, Xudong Qin, and Wenjun Shi
(Shanghai Jiao Tong University, China; East China Normal University, China; IST Austria, Austria)


@InProceedings{PLDI19p248, author = {Peixin Wang and Hongfei Fu and Amir Kafshdar Goharshady and Krishnendu Chatterjee and Xudong Qin and Wenjun Shi}, title = {Cost Analysis of Nondeterministic Probabilistic Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {248-247}, doi = {10.1145/3314221.3314581}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Gen: A General-Purpose Probabilistic Programming System with Programmable Inference
Marco F. Cusumano-Towner, Feras A. Saad, Alexander K. Lew, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA)


@InProceedings{PLDI19p267, author = {Marco F. Cusumano-Towner and Feras A. Saad and Alexander K. Lew and Vikash K. Mansinghka}, title = {Gen: A General-Purpose Probabilistic Programming System with Programmable Inference}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {267-266}, doi = {10.1145/3314221.3314642}, year = {2019}, } Publisher's Version

Incremental Precision-Preserving Symbolic Inference for Probabilistic Programs
Jieyuan Zhang and Jingling Xue
(UNSW, Australia)


@InProceedings{PLDI19p286, author = {Jieyuan Zhang and Jingling Xue}, title = {Incremental Precision-Preserving Symbolic Inference for Probabilistic Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {286-285}, doi = {10.1145/3314221.3314623}, year = {2019}, } Publisher's Version Artifacts Functional

Synthesis

Resource-Guided Program Synthesis
Tristan Knoth, Di Wang, Nadia Polikarpova, and Jan Hoffmann
(University of California at San Diego, USA; Carnegie Mellon University, USA)


@InProceedings{PLDI19p305, author = {Tristan Knoth and Di Wang and Nadia Polikarpova and Jan Hoffmann}, title = {Resource-Guided Program Synthesis}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {305-304}, doi = {10.1145/3314221.3314602}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Using Active Learning to Synthesize Models of Applications That Access Databases
Jiasi Shen and Martin C. Rinard
(Massachusetts Institute of Technology, USA)


@InProceedings{PLDI19p324, author = {Jiasi Shen and Martin C. Rinard}, title = {Using Active Learning to Synthesize Models of Applications That Access Databases}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {324-323}, doi = {10.1145/3314221.3314591}, year = {2019}, } Publisher's Version

Synthesizing Database Programs for Schema Refactoring
Yuepeng Wang, James Dong, Rushi Shah, and Isil Dillig
(University of Texas at Austin, USA)


@InProceedings{PLDI19p343, author = {Yuepeng Wang and James Dong and Rushi Shah and Isil Dillig}, title = {Synthesizing Database Programs for Schema Refactoring}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {343-342}, doi = {10.1145/3314221.3314588}, year = {2019}, } Publisher's Version

Synthesis and Machine Learning for Heterogeneous Extraction
Arun Iyer, Manohar Jonnalagedda, Suresh Parthasarathy, Arjun Radhakrishna, and Sriram K. Rajamani
(Microsoft Research, India; Inpher, Switzerland; Microsoft, USA)


@InProceedings{PLDI19p362, author = {Arun Iyer and Manohar Jonnalagedda and Suresh Parthasarathy and Arjun Radhakrishna and Sriram K. Rajamani}, title = {Synthesis and Machine Learning for Heterogeneous Extraction}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {362-361}, doi = {10.1145/3314221.3322485}, year = {2019}, } Publisher's Version

Memory Management

AutoPersist: An Easy-To-Use Java NVM Framework Based on Reachability
Thomas Shull, Jian Huang, and Josep Torrellas
(University of Illinois at Urbana-Champaign, USA)


@InProceedings{PLDI19p381, author = {Thomas Shull and Jian Huang and Josep Torrellas}, title = {AutoPersist: An Easy-To-Use Java NVM Framework Based on Reachability}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {381-380}, doi = {10.1145/3314221.3314608}, year = {2019}, } Publisher's Version

Mesh: Compacting Memory Management for C/C++ Applications
Bobby Powers, David Tench, Emery D. Berger, and Andrew McGregor
(University of Massachusetts at Amherst, USA)


@InProceedings{PLDI19p400, author = {Bobby Powers and David Tench and Emery D. Berger and Andrew McGregor}, title = {Mesh: Compacting Memory Management for C/C++ Applications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {400-399}, doi = {10.1145/3314221.3314582}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Panthera: Holistic Memory Management for Big Data Processing over Hybrid Memories
Chenxi Wang, Huimin Cui, Ting Cao, John Zigman, Haris Volos, Onur Mutlu, Fang Lv, Xiaobing Feng, and Guoqing Harry Xu
(University of California at Los Angeles, USA; Institute of Computing Technology at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Microsoft Research, USA; University of Sydney, Australia; Google, USA; ETH Zurich, Switzerland)


@InProceedings{PLDI19p419, author = {Chenxi Wang and Huimin Cui and Ting Cao and John Zigman and Haris Volos and Onur Mutlu and Fang Lv and Xiaobing Feng and Guoqing Harry Xu}, title = {Panthera: Holistic Memory Management for Big Data Processing over Hybrid Memories}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {419-418}, doi = {10.1145/3314221.3314650}, year = {2019}, } Publisher's Version

Parsing

Lightweight Multi-Language Syntax Transformation with Parser Parser Combinators
Rijnard van Tonder and Claire Le Goues
(Carnegie Mellon University, USA)


@InProceedings{PLDI19p438, author = {Rijnard van Tonder and Claire Le Goues}, title = {Lightweight Multi-Language Syntax Transformation with Parser Parser Combinators}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {438-437}, doi = {10.1145/3314221.3314589}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

A Typed, Algebraic Approach to Parsing
Neelakantan R. Krishnaswami and Jeremy Yallop
(University of Cambridge, UK)


@InProceedings{PLDI19p457, author = {Neelakantan R. Krishnaswami and Jeremy Yallop}, title = {A Typed, Algebraic Approach to Parsing}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {457-456}, doi = {10.1145/3314221.3314625}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Genie: A Generator of Natural Language Semantic Parsers for Virtual Assistant Commands
Giovanni Campagna, Silei Xu, Mehrad Moradshahi, Richard Socher, and Monica S. Lam
(Stanford University, USA; Salesforce, USA)


@InProceedings{PLDI19p476, author = {Giovanni Campagna and Silei Xu and Mehrad Moradshahi and Richard Socher and Monica S. Lam}, title = {Genie: A Generator of Natural Language Semantic Parsers for Virtual Assistant Commands}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {476-475}, doi = {10.1145/3314221.3314594}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Bug Finding and Testing I

Lazy Counterfactual Symbolic Execution
William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, and Ruzica Piskac
(Yale University, USA; University of California at San Diego, USA)


@InProceedings{PLDI19p495, author = {William T. Hallahan and Anton Xue and Maxwell Troy Bland and Ranjit Jhala and Ruzica Piskac}, title = {Lazy Counterfactual Symbolic Execution}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {495-494}, doi = {10.1145/3314221.3314618}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript
Blake Loring, Duncan Mitchell, and Johannes Kinder
(Royal Holloway University of London, UK; Bundeswehr University Munich, Germany)


@InProceedings{PLDI19p514, author = {Blake Loring and Duncan Mitchell and Johannes Kinder}, title = {Sound Regular Expression Semantics for Dynamic Symbolic Execution of JavaScript}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {514-513}, doi = {10.1145/3314221.3314645}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Effective Floating-Point Analysis via Weak-Distance Minimization
Zhoulai Fu and Zhendong Su
(IT University of Copenhagen, Denmark; ETH Zurich, Switzerland)


@InProceedings{PLDI19p533, author = {Zhoulai Fu and Zhendong Su}, title = {Effective Floating-Point Analysis via Weak-Distance Minimization}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {533-532}, doi = {10.1145/3314221.3314632}, year = {2019}, } Publisher's Version

Parallelism and Super Computing I

Huron: Hybrid False Sharing Detection and Repair
Tanvir Ahmed Khan, Yifan Zhao, Gilles Pokam, Barzan Mozafari, and Baris Kasikci
(University of Michigan, USA; Intel, USA)


@InProceedings{PLDI19p552, author = {Tanvir Ahmed Khan and Yifan Zhao and Gilles Pokam and Barzan Mozafari and Baris Kasikci}, title = {Huron: Hybrid False Sharing Detection and Repair}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {552-551}, doi = {10.1145/3314221.3314644}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Model-Driven Transformations for Multi- and Many-Core CPUs
Martin Kong and Louis-Noël Pouchet
(Brookhaven National Laboratory, USA; Colorado State University, USA)


@InProceedings{PLDI19p571, author = {Martin Kong and Louis-Noël Pouchet}, title = {Model-Driven Transformations for Multi- and Many-Core CPUs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {571-570}, doi = {10.1145/3314221.3314653}, year = {2019}, } Publisher's Version

Parallelism-Centric What-If and Differential Analyses
Adarsh Yoga and Santosh Nagarakatte
(Rutgers University, USA)


@InProceedings{PLDI19p590, author = {Adarsh Yoga and Santosh Nagarakatte}, title = {Parallelism-Centric What-If and Differential Analyses}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {590-589}, doi = {10.1145/3314221.3314621}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Type Systems I

Verifying Message-Passing Programs with Dependent Behavioural Types
Alceste Scalas, Nobuko Yoshida, and Elias Benussi
(Imperial College London, UK; Aston University, UK; Faculty Science, UK)


@InProceedings{PLDI19p609, author = {Alceste Scalas and Nobuko Yoshida and Elias Benussi}, title = {Verifying Message-Passing Programs with Dependent Behavioural Types}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {609-608}, doi = {10.1145/3314221.3322484}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Toward Efficient Gradual Typing for Structural Types via Coercions
Andre Kuhlenschmidt, Deyaaeldeen Almahallawi, and Jeremy G. Siek
(Indiana University, USA)


@InProceedings{PLDI19p628, author = {Andre Kuhlenschmidt and Deyaaeldeen Almahallawi and Jeremy G. Siek}, title = {Toward Efficient Gradual Typing for Structural Types via Coercions}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {628-627}, doi = {10.1145/3314221.3314627}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Bidirectional Type Checking for Relational Properties
Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, and Deepak Garg
(Facebook, USA; SUNY Buffalo, USA; MPI for Security and Privacy, Germany; IMDEA Software Institute, Spain; MPI-SWS, Germany)


@InProceedings{PLDI19p647, author = {Ezgi Çiçek and Weihao Qu and Gilles Barthe and Marco Gaboardi and Deepak Garg}, title = {Bidirectional Type Checking for Relational Properties}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {647-646}, doi = {10.1145/3314221.3314603}, year = {2019}, } Publisher's Version

Bug Finding and Testing II

Parser-Directed Fuzzing
Björn Mathis, Rahul Gopinath, Michaël Mera, Alexander Kampmann, Matthias Höschele, and Andreas Zeller
(CISPA, Germany)


@InProceedings{PLDI19p666, author = {Björn Mathis and Rahul Gopinath and Michaël Mera and Alexander Kampmann and Matthias Höschele and Andreas Zeller}, title = {Parser-Directed Fuzzing}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {666-665}, doi = {10.1145/3314221.3314651}, year = {2019}, } Publisher's Version

Continuously Reasoning about Programs using Differential Bayesian Inference
Kihong Heo, Mukund Raghothaman, Xujie Si, and Mayur Naik
(University of Pennsylvania, USA)


@InProceedings{PLDI19p685, author = {Kihong Heo and Mukund Raghothaman and Xujie Si and Mayur Naik}, title = {Continuously Reasoning about Programs using Differential Bayesian Inference}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {685-684}, doi = {10.1145/3314221.3314616}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Sparse Record and Replay with Controlled Scheduling
Christopher Lidbury and Alastair F. Donaldson
(Imperial College London, UK)


@InProceedings{PLDI19p704, author = {Christopher Lidbury and Alastair F. Donaldson}, title = {Sparse Record and Replay with Controlled Scheduling}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {704-703}, doi = {10.1145/3314221.3314635}, year = {2019}, } Publisher's Version

Parallelism and Super Computing II

Sparse Computation Data Dependence Simplification for Efficient Compiler-Generated Inspectors
Mahdi Soltan Mohammadi, Tomofumi Yuki, Kazem Cheshmi, Eddie C. Davis, Mary Hall, Maryam Mehri Dehnavi, Payal Nandy, Catherine Olschanowsky, Anand Venkat, and Michelle Mills Strout
(University of Arizona, USA; Inria, France; University of Rennes, France; CNRS, France; IRISA, France; University of Toronto, Canada; Boise State University, USA; University of Utah, USA; Intel, USA)


@InProceedings{PLDI19p723, author = {Mahdi Soltan Mohammadi and Tomofumi Yuki and Kazem Cheshmi and Eddie C. Davis and Mary Hall and Maryam Mehri Dehnavi and Payal Nandy and Catherine Olschanowsky and Anand Venkat and Michelle Mills Strout}, title = {Sparse Computation Data Dependence Simplification for Efficient Compiler-Generated Inspectors}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {723-722}, doi = {10.1145/3314221.3314646}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Modular Divide-and-Conquer Parallelization of Nested Loops
Azadeh Farzan and Victor Nicolet
(University of Toronto, Canada)


@InProceedings{PLDI19p742, author = {Azadeh Farzan and Victor Nicolet}, title = {Modular Divide-and-Conquer Parallelization of Nested Loops}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {742-741}, doi = {10.1145/3314221.3314612}, year = {2019}, } Publisher's Version

Generating Piecewise-Regular Code from Irregular Structures
Travis Augustine, Janarthanan Sarma, Louis-Noël Pouchet, and Gabriel Rodríguez
(Colorado State University, USA; Universidade da Coruña, Spain)


@InProceedings{PLDI19p761, author = {Travis Augustine and Janarthanan Sarma and Louis-Noël Pouchet and Gabriel Rodríguez}, title = {Generating Piecewise-Regular Code from Irregular Structures}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {761-760}, doi = {10.1145/3314221.3314615}, year = {2019}, } Publisher's Version Artifacts Functional

Type Systems II

ILC: A Calculus for Composable, Computational Cryptography
Kevin Liao, Matthew A. Hammer, and Andrew Miller
(University of Illinois at Urbana-Champaign, USA; DFINITY, USA)


@InProceedings{PLDI19p780, author = {Kevin Liao and Matthew A. Hammer and Andrew Miller}, title = {ILC: A Calculus for Composable, Computational Cryptography}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {780-779}, doi = {10.1145/3314221.3314607}, year = {2019}, } Publisher's Version

Proving Differential Privacy with Shadow Execution
Yuxin Wang, Zeyu Ding, Guanhong Wang, Daniel Kifer, and Danfeng Zhang
(Pennsylvania State University, USA)


@InProceedings{PLDI19p799, author = {Yuxin Wang and Zeyu Ding and Guanhong Wang and Daniel Kifer and Danfeng Zhang}, title = {Proving Differential Privacy with Shadow Execution}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {799-798}, doi = {10.1145/3314221.3314619}, year = {2019}, } Publisher's Version

Data-Trace Types for Distributed Stream Processing Systems
Konstantinos Mamouras, Caleb Stanford, Rajeev Alur, Zachary G. Ives, and Val Tannen
(Rice University, USA; University of Pennsylvania, USA)


@InProceedings{PLDI19p818, author = {Konstantinos Mamouras and Caleb Stanford and Rajeev Alur and Zachary G. Ives and Val Tannen}, title = {Data-Trace Types for Distributed Stream Processing Systems}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {818-817}, doi = {10.1145/3314221.3314580}, year = {2019}, } Publisher's Version

ML

An Inductive Synthesis Framework for Verifiable Reinforcement Learning
He Zhu, Zikang Xiong, Stephen Magill, and Suresh Jagannathan
(Galois, USA; Purdue University, USA)


@InProceedings{PLDI19p837, author = {He Zhu and Zikang Xiong and Stephen Magill and Suresh Jagannathan}, title = {An Inductive Synthesis Framework for Verifiable Reinforcement Learning}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {837-836}, doi = {10.1145/3314221.3314638}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Programming Support for Autonomizing Software
Wen-Chuan Lee, Peng Liu, Yingqi Liu, Shiqing Ma, and Xiangyu Zhang
(Purdue University, USA; IBM, USA)


@InProceedings{PLDI19p856, author = {Wen-Chuan Lee and Peng Liu and Yingqi Liu and Shiqing Ma and Xiangyu Zhang}, title = {Programming Support for Autonomizing Software}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {856-855}, doi = {10.1145/3314221.3314593}, year = {2019}, } Publisher's Version

Wootz: A Compiler-Based Framework for Fast CNN Pruning via Composability
Hui Guan, Xipeng Shen, and Seung-Hwan Lim
(North Carolina State University, USA; Oak Ridge National Laboratory, USA)


@InProceedings{PLDI19p875, author = {Hui Guan and Xipeng Shen and Seung-Hwan Lim}, title = {Wootz: A Compiler-Based Framework for Fast CNN Pruning via Composability}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {875-874}, doi = {10.1145/3314221.3314652}, year = {2019}, } Publisher's Version

Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness
Greg Anderson, Shankara Pailoor, Isil Dillig, and Swarat Chaudhuri
(University of Texas at Austin, USA; Rice University, USA)


@InProceedings{PLDI19p894, author = {Greg Anderson and Shankara Pailoor and Isil Dillig and Swarat Chaudhuri}, title = {Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {894-893}, doi = {10.1145/3314221.3314614}, year = {2019}, } Publisher's Version

Specification

Unsupervised Learning of API Aliasing Specifications
Jan Eberhardt, Samuel Steffen, Veselin Raychev, and Martin Vechev
(DeepCode, Switzerland; ETH Zurich, Switzerland)


@InProceedings{PLDI19p913, author = {Jan Eberhardt and Samuel Steffen and Veselin Raychev and Martin Vechev}, title = {Unsupervised Learning of API Aliasing Specifications}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {913-912}, doi = {10.1145/3314221.3314640}, year = {2019}, } Publisher's Version

Scalable Taint Specification Inference with Big Code
Victor Chibotaru, Benjamin Bichsel, Veselin Raychev, and Martin Vechev
(DeepCode, Switzerland; ETH Zurich, Switzerland)


@InProceedings{PLDI19p932, author = {Victor Chibotaru and Benjamin Bichsel and Veselin Raychev and Martin Vechev}, title = {Scalable Taint Specification Inference with Big Code}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {932-931}, doi = {10.1145/3314221.3314648}, year = {2019}, } Publisher's Version

Learning Stateful Preconditions Modulo a Test Generator
Angello Astorga, P. Madhusudan, Shambwaditya Saha, Shiyu Wang, and Tao Xie
(University of Illinois at Urbana-Champaign, USA)


@InProceedings{PLDI19p951, author = {Angello Astorga and P. Madhusudan and Shambwaditya Saha and Shiyu Wang and Tao Xie}, title = {Learning Stateful Preconditions Modulo a Test Generator}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {951-950}, doi = {10.1145/3314221.3314641}, year = {2019}, } Publisher's Version

SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic
Ton Chanh Le, Guolong Zheng, and ThanhVu Nguyen
(Stevens Institute of Technology, USA; University of Nebraska-Lincoln, USA)


@InProceedings{PLDI19p970, author = {Ton Chanh Le and Guolong Zheng and ThanhVu Nguyen}, title = {SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {970-969}, doi = {10.1145/3314221.3314634}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Static Analysis

Abstract Interpretation under Speculative Execution
Meng Wu and Chao Wang
(Virginia Tech, USA; University of Southern California, USA)


@InProceedings{PLDI19p989, author = {Meng Wu and Chao Wang}, title = {Abstract Interpretation under Speculative Execution}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {989-988}, doi = {10.1145/3314221.3314647}, year = {2019}, } Publisher's Version

A Fast Analytical Model of Fully Associative Caches
Tobias Gysi, Tobias Grosser, Laurin Brandner, and Torsten Hoefler
(ETH Zurich, Switzerland)


@InProceedings{PLDI19p1008, author = {Tobias Gysi and Tobias Grosser and Laurin Brandner and Torsten Hoefler}, title = {A Fast Analytical Model of Fully Associative Caches}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1008-1007}, doi = {10.1145/3314221.3314606}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Sound, Fine-Grained Traversal Fusion for Heterogeneous Trees
Laith Sakka, Kirshanthan Sundararajah, Ryan R. Newton, and Milind Kulkarni
(Purdue University, USA; Indiana University, USA)


@InProceedings{PLDI19p1027, author = {Laith Sakka and Kirshanthan Sundararajah and Ryan R. Newton and Milind Kulkarni}, title = {Sound, Fine-Grained Traversal Fusion for Heterogeneous Trees}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1027-1026}, doi = {10.1145/3314221.3314626}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Size-Change Termination as a Contract: Dynamically and Statically Enforcing Termination for Higher-Order Programs
Phúc C. Nguyễn, Thomas Gilray, Sam Tobin-Hochstadt, and David Van Horn
(University of Maryland at College Park, USA; University of Alabama at Birmingham, USA; Indiana University, USA)


@InProceedings{PLDI19p1046, author = {Phúc C. Nguyễn and Thomas Gilray and Sam Tobin-Hochstadt and David Van Horn}, title = {Size-Change Termination as a Contract: Dynamically and Statically Enforcing Termination for Higher-Order Programs}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1046-1045}, doi = {10.1145/3314221.3314643}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Dynamics: Analysis and Compilation

SemCluster: Clustering of Imperative Programming Assignments Based on Quantitative Semantic Features
David M. Perry, Dohyeong Kim, Roopsha Samanta, and Xiangyu Zhang
(Purdue University, USA)


@InProceedings{PLDI19p1065, author = {David M. Perry and Dohyeong Kim and Roopsha Samanta and Xiangyu Zhang}, title = {SemCluster: Clustering of Imperative Programming Assignments Based on Quantitative Semantic Features}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1065-1064}, doi = {10.1145/3314221.3314629}, year = {2019}, } Publisher's Version

Computing Summaries of String Loops in C for Better Testing and Refactoring
Timotej Kapus, Oren Ish-Shalom, Shachar Itzhaky, Noam Rinetzky, and Cristian Cadar
(Imperial College London, UK; Tel Aviv University, Israel; Technion, Israel)


@InProceedings{PLDI19p1084, author = {Timotej Kapus and Oren Ish-Shalom and Shachar Itzhaky and Noam Rinetzky and Cristian Cadar}, title = {Computing Summaries of String Loops in C for Better Testing and Refactoring}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1084-1083}, doi = {10.1145/3314221.3314610}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Reusable Inline Caching for JavaScript Performance
Jiho Choi, Thomas Shull, and Josep Torrellas
(University of Illinois at Urbana-Champaign, USA)


@InProceedings{PLDI19p1103, author = {Jiho Choi and Thomas Shull and Josep Torrellas}, title = {Reusable Inline Caching for JavaScript Performance}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1103-1102}, doi = {10.1145/3314221.3314587}, year = {2019}, } Publisher's Version

Performance

Composable, Sound Transformations of Nested Recursion and Loops
Kirshanthan Sundararajah and Milind Kulkarni
(Purdue University, USA)


@InProceedings{PLDI19p1122, author = {Kirshanthan Sundararajah and Milind Kulkarni}, title = {Composable, Sound Transformations of Nested Recursion and Loops}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1122-1121}, doi = {10.1145/3314221.3314592}, year = {2019}, } Publisher's Version

Low-Latency Graph Streaming using Compressed Purely-Functional Trees
Laxman Dhulipala, Guy E. Blelloch, and Julian Shun
(Carnegie Mellon University, USA; Massachusetts Institute of Technology, USA)


@InProceedings{PLDI19p1141, author = {Laxman Dhulipala and Guy E. Blelloch and Julian Shun}, title = {Low-Latency Graph Streaming using Compressed Purely-Functional Trees}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1141-1140}, doi = {10.1145/3314221.3314598}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Co-optimizing Memory-Level Parallelism and Cache-Level Parallelism
Xulong Tang, Mahmut Taylan Kandemir, Mustafa Karakoy, and Meenakshi Arunachalam
(Pennsylvania State University, USA; TOBB University of Economics and Technology, Turkey; Intel, USA)


@InProceedings{PLDI19p1160, author = {Xulong Tang and Mahmut Taylan Kandemir and Mustafa Karakoy and Meenakshi Arunachalam}, title = {Co-optimizing Memory-Level Parallelism and Cache-Level Parallelism}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1160-1159}, doi = {10.1145/3314221.3314599}, year = {2019}, } Publisher's Version

Type Systems III

Characterising Renaming within OCaml’s Module System: Theory and Implementation
Reuben N. S. Rowe, Hugo Férée, Simon J. Thompson, and Scott Owens
(University of Kent, UK)


@InProceedings{PLDI19p1179, author = {Reuben N. S. Rowe and Hugo Férée and Simon J. Thompson and Scott Owens}, title = {Characterising Renaming within OCaml’s Module System: Theory and Implementation}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1179-1178}, doi = {10.1145/3314221.3314600}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Type-Level Computations for Ruby Libraries
Milod Kazerounian, Sankha Narayan Guria, Niki Vazou, Jeffrey S. Foster, and David Van Horn
(University of Maryland at College Park, USA; IMDEA Software Institute, Spain; Tufts University, USA)


@InProceedings{PLDI19p1198, author = {Milod Kazerounian and Sankha Narayan Guria and Niki Vazou and Jeffrey S. Foster and David Van Horn}, title = {Type-Level Computations for Ruby Libraries}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1198-1197}, doi = {10.1145/3314221.3314630}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Systems I

Replication-Aware Linearizability
Chao Wang, Constantin Enea, Suha Orhun Mutluergil, and Gustavo Petri
(IRIF, France; University Paris Diderot, France; CNRS, France; ARM, UK)


@InProceedings{PLDI19p1217, author = {Chao Wang and Constantin Enea and Suha Orhun Mutluergil and Gustavo Petri}, title = {Replication-Aware Linearizability}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1217-1216}, doi = {10.1145/3314221.3314617}, year = {2019}, } Publisher's Version

DFix: Automatically Fixing Timing Bugs in Distributed Systems
Guangpu Li, Haopeng Liu, Xianglan Chen, Haryadi S. Gunawi, and Shan Lu
(University of Chicago, USA; University of Science and Technology of China, China)


@InProceedings{PLDI19p1236, author = {Guangpu Li and Haopeng Liu and Xianglan Chen and Haryadi S. Gunawi and Shan Lu}, title = {DFix: Automatically Fixing Timing Bugs in Distributed Systems}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1236-1235}, doi = {10.1145/3314221.3314620}, year = {2019}, } Publisher's Version

Ignis: Scaling Distribution-Oblivious Systems with Light-Touch Distribution
Nikos Vasilakis, Ben Karel, Yash Palkhiwala, John Sonchack, André DeHon, and Jonathan M. Smith
(University of Pennsylvania, USA)


@InProceedings{PLDI19p1255, author = {Nikos Vasilakis and Ben Karel and Yash Palkhiwala and John Sonchack and André DeHon and Jonathan M. Smith}, title = {Ignis: Scaling Distribution-Oblivious Systems with Light-Touch Distribution}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1255-1254}, doi = {10.1145/3314221.3314586}, year = {2019}, } Publisher's Version

Verification I

Semantic Program Alignment for Equivalence Checking
Berkeley Churchill, Oded Padon, Rahul Sharma, and Alex Aiken
(Stanford University, USA; Microsoft Research, India)


@InProceedings{PLDI19p1274, author = {Berkeley Churchill and Oded Padon and Rahul Sharma and Alex Aiken}, title = {Semantic Program Alignment for Equivalence Checking}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1274-1273}, doi = {10.1145/3314221.3314596}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Verified Compilation on a Verified Processor
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony Fox
(Chalmers University of Technology, Sweden; DeepMind, UK; Carnegie Mellon University, USA; Data61 at CSIRO, Australia; Australian National University, Australia; ARM, UK)


@InProceedings{PLDI19p1293, author = {Andreas Lööw and Ramana Kumar and Yong Kiam Tan and Magnus O. Myreen and Michael Norrish and Oskar Abrahamsson and Anthony Fox}, title = {Verified Compilation on a Verified Processor}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1293-1292}, doi = {10.1145/3314221.3314622}, year = {2019}, } Publisher's Version Artifacts Functional

Argosy: Verifying Layered Storage Systems with Recovery Refinement
Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich
(Massachusetts Institute of Technology, USA)


@InProceedings{PLDI19p1312, author = {Tej Chajed and Joseph Tassarotti and M. Frans Kaashoek and Nickolai Zeldovich}, title = {Argosy: Verifying Layered Storage Systems with Recovery Refinement}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1312-1311}, doi = {10.1145/3314221.3314585}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Systems II

Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions
Elazar Gershuni, Nadav Amit, Arie Gurfinkel, Nina Narodytska, Jorge A. Navas, Noam Rinetzky, Leonid Ryzhyk, and Mooly Sagiv
(VMware, USA; Tel Aviv University, Israel; University of Waterloo, Canada; SRI International, USA)


@InProceedings{PLDI19p1331, author = {Elazar Gershuni and Nadav Amit and Arie Gurfinkel and Nina Narodytska and Jorge A. Navas and Noam Rinetzky and Leonid Ryzhyk and Mooly Sagiv}, title = {Simple and Precise Static Analysis of Untrusted Linux Kernel Extensions}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1331-1330}, doi = {10.1145/3314221.3314590}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Transactional Concurrency Control for Intermittent, Energy-Harvesting Computing Systems
Emily Ruppel and Brandon Lucia
(Carnegie Mellon University, USA)


@InProceedings{PLDI19p1350, author = {Emily Ruppel and Brandon Lucia}, title = {Transactional Concurrency Control for Intermittent, Energy-Harvesting Computing Systems}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1350-1349}, doi = {10.1145/3314221.3314583}, year = {2019}, } Publisher's Version

Supporting Peripherals in Intermittent Systems with Just-In-Time Checkpoints
Kiwan Maeng and Brandon Lucia
(Carnegie Mellon University, USA)


@InProceedings{PLDI19p1369, author = {Kiwan Maeng and Brandon Lucia}, title = {Supporting Peripherals in Intermittent Systems with Just-In-Time Checkpoints}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1369-1368}, doi = {10.1145/3314221.3314613}, year = {2019}, } Publisher's Version

Verification II

Verification of Programs under the Release-Acquire Semantics
Parosh Aziz Abdulla, Jatin Arora, Mohamed Faouzi Atig, and Shankaranarayanan Krishna
(Uppsala University, Sweden; IIT Bombay, India)


@InProceedings{PLDI19p1388, author = {Parosh Aziz Abdulla and Jatin Arora and Mohamed Faouzi Atig and Shankaranarayanan Krishna}, title = {Verification of Programs under the Release-Acquire Semantics}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1388-1387}, doi = {10.1145/3314221.3314649}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture
Sandeep Dasgupta, Daejun Park, Theodoros Kasampalis, Vikram S. Adve, and Grigore Roşu
(University of Illinois at Urbana-Champaign, USA; Runtime Verification, USA)


@InProceedings{PLDI19p1407, author = {Sandeep Dasgupta and Daejun Park and Theodoros Kasampalis and Vikram S. Adve and Grigore Roşu}, title = {A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1407-1406}, doi = {10.1145/3314221.3314601}, year = {2019}, } Publisher's Version Published Artifact Artifacts Available Artifacts Functional

An Applied Quantum Hoare Logic
Li Zhou, Nengkun Yu, and Mingsheng Ying
(Tsinghua University, China; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China)


@InProceedings{PLDI19p1426, author = {Li Zhou and Nengkun Yu and Mingsheng Ying}, title = {An Applied Quantum Hoare Logic}, booktitle = {Proc.\ PLDI}, publisher = {ACM}, pages = {1426-1425}, doi = {10.1145/3314221.3314584}, year = {2019}, } Publisher's Version

proc time: 0.88