![](https://dblp.dagstuhl.de/img/logo.ua.320x120.png)
![](https://dblp.dagstuhl.de/img/dropdown.dark.16x16.png)
![](https://dblp.dagstuhl.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
![search dblp](https://dblp.dagstuhl.de/img/search.dark.16x16.png)
default search action
PLDI 2021: Virtual Event, Canada
- Stephen N. Freund, Eran Yahav:
PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021. ACM 2021, ISBN 978-1-4503-8391-2 - Tamás Szabó
, Sebastian Erdweg
, Gábor Bergmann
:
Incremental whole-program analysis in Datalog with lattices. 1-15 - Kyeongmin Cho
, Sung-Hwan Lee
, Azalea Raad, Jeehoon Kang
:
Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8. 16-31 - Kia Rahmani, Kartik Nagar
, Benjamin Delaware, Suresh Jagannathan:
Repairing serializability bugs in distributed database programs via automated schema refactoring. 32-47 - Runzhou Tao
, Yunong Shi, Jianan Yao
, John Hui, Frederic T. Chong
, Ronghui Gu
:
Gleipnir: toward practical error analysis for Quantum programs. 48-64 - Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr:
Alive2: bounded translation validation for LLVM. 65-79 - Simon Spies, Lennard Gäher, Daniel Gratzer
, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
:
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. 80-95 - Alex Reinking
, Ningning Xie, Leonardo de Moura, Daan Leijen:
Perceus: garbage free reference counting with reuse. 96-111 - Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, Dan Grossman:
Proof repair across type equivalences. 112-127 - Rodrigo Bruno
, Vojin Jovanovic, Christian Wimmer, Gustavo Alonso:
Compiler-assisted object inlining with value fields. 128-141 - Xiaolei Ren
, Michael Ho, Jiang Ming, Yu Lei, Li Li:
Unleashing the hidden power of compiler optimization on binary code difference: an empirical study. 142-157 - Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg
:
RefinedC: automating the foundational verification of C code with refined ownership types. 158-174 - Michael Christensen
, Timothy Sherwood
, Jonathan Balkind
, Ben Hardekopf
:
Wire sorts: a language abstraction for safe hardware composition. 175-189 - Wookeun Jung
, Thanh Tuan Dao
, Jaejin Lee
:
DeepCuts: a deep learning optimization framework for versatile GPU workloads. 190-205 - K. C. Sivaramakrishnan
, Stephen Dolan, Leo White, Tom Kelly, Sadiq Jaffer, Anil Madhavapeddy
:
Retrofitting effect handlers onto OCaml. 206-221 - Anouk Paradis, Benjamin Bichsel, Samuel Steffen, Martin T. Vechev:
Unqomp: synthesizing uncomputation in Quantum circuits. 222-236 - David Castro-Perez, Francisco Ferreira
, Lorenzo Gheri
, Nobuko Yoshida
:
Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes. 237-251 - Huaipan Jiang, Haibo Zhang, Xulong Tang
, Vineetha Govindaraj, Jack Sampson, Mahmut Taylan Kandemir, Danfeng Zhang
:
Fluid: a framework for approximate concurrency via controlled dependency relaxation. 252-267 - Paschalis Mpeis
, Pavlos Petoumenos
, Kim M. Hazelwood
, Hugh Leather
:
Developer and user-transparent compiler optimization for interactive applications. 268-281 - Benno Stein, Bor-Yuh Evan Chang
, Manu Sridharan
:
Demanded abstract interpretation. 282-295 - Jingxuan He
, Cheng-Chun Lee, Veselin Raychev, Martin T. Vechev:
Learning to find naming issues with big code and small supervision. 296-311 - Michael H. Fischer, Giovanni Campagna, Euirim Choi, Monica S. Lam:
DIY assistant: a multi-modal end-user programmable virtual assistant. 312-327 - Qiaochu Chen, Aaron Lamoreaux, Xinyu Wang
, Greg Durrett, Osbert Bastani, Isil Dillig:
Web question answering with neurosymbolic program synthesis. 328-343 - Sankha Narayan Guria, Jeffrey S. Foster, David Van Horn
:
RbSyn: type- and effect-guided program synthesis. 344-358 - Jay P. Lim
, Santosh Nagarakatte
:
High performance correctly rounded math libraries for 32-bit floating point representations. 359-374 - Meghan Cowan
, Deeksha Dangwal
, Armin Alaghi, Caroline Trippel
, Vincent T. Lee, Brandon Reagen:
Porcupine: a synthesizing compiler for vectorized homomorphic encryption. 375-389 - Ridwan Salihin Shariffdeen
, Yannic Noller
, Lars Grunske
, Abhik Roychoudhury
:
Concolic program repair. 390-405 - Sebastian Erdweg
, Tamás Szabó
, André Pacak:
Concise, type-safe, and efficient structural diffing. 406-419 - Sam Lasser, Chris Casinghino, Kathleen Fisher, Cody Roux:
CoStar: a verified ALL(*) parser. 420-434 - Guixin Ye
, Zhanyong Tang, Shin Hwei Tan
, Songfang Huang, Dingyi Fang, Xiaoyang Sun, Lizhong Bian, Haibo Wang, Zheng Wang
:
Automated conformance testing for JavaScript engines via deep compiler fuzzing. 435-450 - Yurii Kostyukov
, Dmitry Mordvinov
, Grigory Fedyukovich
:
Beyond the elementary representations of program invariants over algebraic data types. 451-465 - Gregory Bonaert
, Dimitar I. Dimitrov
, Maximilian Baader
, Martin T. Vechev:
Fast and precise certification of transformers. 466-481 - Benoît Montagu
, Thomas P. Jensen:
Trace-based control-flow analysis. 482-496 - Guillaume Baudart, Javier Burroni, Martin Hirzel, Louis Mandel, Avraham Shinnar:
Compiling Stan to generative probabilistic languages and extension to deep probabilistic programming. 497-510 - Cyrus Omar
, David Moon
, Andrew Blinn
, Ian Voysey
, Nick Collins
, Ravi Chugh
:
Filling typed holes with live GUIs. 511-525 - Daniel Anderson
, Guy E. Blelloch
, Yuanhao Wei
:
Concurrent deferred reference counting with constant-time overhead. 526-541 - Nengkun Yu
, Jens Palsberg
:
Quantum abstract interpretation. 542-558 - Di Wang
, Jan Hoffmann, Thomas W. Reps:
Central moment analysis for cost accumulators in probabilistic programs. 559-573 - Shankara Pailoor, Yuepeng Wang, Xinyu Wang
, Isil Dillig:
Synthesizing data structure refinements from integrity constraints. 574-587 - Matthew Sotoudeh
, Aditya V. Thakur
:
Provable repair of deep neural networks. 588-603 - Andres Erbsen
, Samuel Gruetter
, Joonwon Choi
, Clark Wood, Adam Chlipala:
Integration verification across software and hardware for a simple embedded system. 604-619 - Caleb Stanford
, Margus Veanes, Nikolaj S. Bjørner:
Symbolic Boolean derivatives for efficiently solving extended regular expression constraints. 620-635 - Hongjin Liang, Xinyu Feng:
Abstraction for conflict-free replicated data types. 636-650 - Dongpeng Xu
, Binbin Liu, Weijie Feng, Jiang Ming, Qilong Zheng, Jing Li, Qiaoyan Yu
:
Boosting SMT solver performance on mixed-bitwise-arithmetic expressions. 651-664 - Mahmut Taylan Kandemir, Xulong Tang
, Hui Zhao
, Jihyun Ryoo
, Mustafa Karaköy
:
Distance-in-time versus distance-in-space. 665-680 - Xiaowen Hu
, David Zhao
, Herbert Jordan
, Bernhard Scholz
:
An efficient interpreter for Datalog by de-specializing relations. 681-695 - Jason R. Koenig
, Oded Padon, Alex Aiken:
Adaptive restarts for stochastic synthesis. 696-709 - John Renner, Alex Sanchez-Stern, Fraser Brown, Sorin Lerner, Deian Stefan:
Scooter & Sidecar: a domain-specific approach to writing secure database migrations. 710-724 - Bozhen Liu
, Peiming Liu, Yanze Li, Chia-Che Tsai, Dilma Da Silva, Jeff Huang
:
When threads meet events: efficient and precise static race detection with origins. 725-739 - Cosku Acay
, Rolph Recto, Joshua Gancher, Andrew C. Myers, Elaine Shi:
Viaduct: an extensible, optimizing compiler for secure distributed programs. 740-755 - Luis Vega
, Joseph McMahan, Adrian Sampson, Dan Grossman, Luis Ceze:
Reticle: a virtual machine for programming modern FPGAs. 756-771 - Ali Asadi, Krishnendu Chatterjee
, Hongfei Fu
, Amir Kafshdar Goharshady
, Mohammad Mahdavi:
Polynomial reachability witnesses via Stellensätze. 772-787 - Di Wang
, Jan Hoffmann, Thomas W. Reps:
Sound probabilistic inference via guide types. 788-803 - Feras A. Saad
, Martin C. Rinard, Vikash K. Mansinghka:
SPPL: probabilistic programming with fast exact symbolic inference. 804-819 - Akimasa Morihata
, Shigeyuki Sato
:
Reverse engineering for reduction parallelization via semiring polynomials. 820-834 - Kevin Ellis, Catherine Wong, Maxwell I. Nye, Mathias Sablé-Meyer, Lucas Morales
, Luke B. Hewitt, Luc Cary, Armando Solar-Lezama
, Joshua B. Tenenbaum:
DreamCoder: bootstrapping inductive program synthesis with wake-sleep library learning. 835-850 - Milijana Surbatovich
, Limin Jia
, Brandon Lucia:
Automatically enforcing fresh and consistent inputs in intermittent systems. 851-866 - Minki Cho
, Sung-Hwan Lee
, Chung-Kil Hur, Ori Lahav
:
Modular data-race-freedom guarantees in the promising semantics. 867-882 - Wei Niu
, Jiexiong Guan, Yanzhi Wang, Gagan Agrawal, Bin Ren:
DNNFusion: accelerating deep neural networks execution with advanced operator fusion. 883-898 - Yoshiki Takashima, Ruben Martins, Limin Jia
, Corina S. Pasareanu:
SyRust: automatic testing of Rust libraries with semantic-aware program synthesis. 899-913 - Zhiqiang Zuo, Yiyu Zhang, Qiuhong Pan, Shenming Lu, Yue Li, Linzhang Wang, Xuandong Li, Guoqing Harry Xu:
Chianina: an evolving graph system for flow- and context-sensitive analyses of million lines of C code. 914-929 - Qingkai Shi
, Peisen Yao
, Rongxin Wu
, Charles Zhang:
Path-sensitive sparse analysis without path conditions. 930-943 - Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe
, Ilya Sergey:
Cyclic program synthesis. 944-959 - Krzysztof Maziarz, Tom Ellis, Alan Lawrence, Andrew W. Fitzgibbon, Simon Peyton Jones:
Hashing modulo alpha-equivalence. 960-973 - Azadeh Farzan, Victor Nicolet:
Phased synthesis of divide and conquer programs. 974-986 - Ruslan Nikolaev
, Binoy Ravindran:
Snapshot-free, transparent, and robust memory reclamation for lock-free data structures. 987-1002 - Christian Gram Kalhauge
, Jens Palsberg
:
Logical bytecode reduction. 1003-1016 - Alastair F. Donaldson
, Paul Thomson, Vasyl Teliman, Stefano Milizia, André Perez Maselco, Antoni Karpinski:
Test-case reduction and deduplication almost for free with transformation-based compiler testing. 1017-1032 - Krishnendu Chatterjee
, Ehsan Kafshdar Goharshady, Petr Novotný
, Dorde Zikelic:
Proving non-termination by program reversal. 1033-1048 - Raghav Malik
, Vidush Singhal
, Benjamin Gottfried, Milind Kulkarni
:
Vectorized secure evaluation of decision forests. 1049-1063 - Mike Rainey, Ryan R. Newton, Kyle C. Hale
, Nikos Hardavellas
, Simone Campanoni, Peter A. Dinda, Umut A. Acar:
Task parallel assembly language for uncompromising parallelism. 1064-1079 - Zhiqiang Zuo, Kai Ji, Yifei Wang, Wei Tao, Linzhang Wang, Xuandong Li, Guoqing Harry Xu:
JPortal: precise and efficient control-flow tracing for JVM programs with Intel processor trace. 1080-1094 - Jérémie Koenig
, Zhong Shao
:
CompCertO: compiling certified open C components. 1095-1109 - Aalok Thakkar, Aaditya Naik, Nathaniel Sands, Rajeev Alur, Mayur Naik, Mukund Raghothaman
:
Example-guided synthesis of relational queries. 1110-1125 - Yuandao Cai, Peisen Yao
, Charles Zhang:
Canary: practical static detection of inter-thread value-flow bugs. 1126-1140 - Matthew Mirman, Alexander Hägele, Pavol Bielik, Timon Gehr, Martin T. Vechev:
Robustness certification with generative models. 1141-1154 - Gefei Zuo
, Jiacheng Ma
, Andrew Quinn
, Pramod Bhatotia, Pedro Fonseca, Baris Kasikci
:
Execution reconstruction: harnessing failure reoccurrences for failure reproduction. 1155-1170 - Jinyi Wang, Yican Sun, Hongfei Fu
, Krishnendu Chatterjee
, Amir Kafshdar Goharshady
:
Quantitative analysis of assertion violations in probabilistic programs. 1171-1186 - Auguste Olivry, Guillaume Iooss, Nicolas Tollenaere, Atanas Rountev, P. Sadayappan, Fabrice Rastello:
IOOpt: automatic derivation of I/O complexity bounds for affine programs. 1187-1202 - Sumanth Prabhu S, Grigory Fedyukovich, Kumar Madhukar, Deepak D'Souza:
Specification synthesis with constrained Horn clauses. 1203-1217 - Michal Friedman
, Erez Petrank, Pedro Ramalhete:
Mirror: making lock-free data structures persistent. 1218-1232 - Jie Zhao
, Bojie Li, Wang Nie, Zhen Geng, Renwei Zhang, Xiong Gao, Bin Cheng, Chen Wu, Yun Cheng, Zheng Li, Peng Di
, Kun Zhang, Xuefeng Jin:
AKG: automatic kernel generation for neural processing units using polyhedral transformations. 1233-1248 - Nilanjana Basu, Claudio Montanari, Jakob Eriksson:
Frequent background polling on a shared thread, using light-weight compiler interrupts. 1249-1263 - Fei He
, Zhihang Sun, Hongyu Fan:
Satisfiability modulo ordering consistency theory for multi-threaded program verification. 1264-1279 - Rohan Basu Roy, Tirthak Patel
, Vijay Gadepally, Devesh Tiwari:
Bliss: auto-tuning complex applications using a pool of diverse lightweight learning models. 1280-1295 - Shaowei Zhu
, Zachary Kincaid
:
Termination analysis without the tears. 1296-1311 - Raven Beutner
, Luke Ong:
On probabilistic termination of functional programs with continuous distributions. 1312-1326 - George Pîrlea
, Amrit Kumar, Ilya Sergey:
Practical smart contract sharding with ownership and commutativity analysis. 1327-1341
![](https://dblp.dagstuhl.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.