Table of Contents

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