Abstract is missing.
- Modular information flow through ownershipWill Crichton, Marco Patrignani, Maneesh Agrawala, Pat Hanrahan. 1-14 [doi]
- ANOSY: approximated knowledge synthesis with refinement types for declassificationSankha Narayan Guria, Niki Vazou, Marco Guarnieri, James Parker. 15-30 [doi]
- Hardening attack surfaces with formally proven binary format parsersNikhil Swamy, Tahina Ramananandro, Aseem Rastogi, Irina Spiridonova, Haobin Ni, Dmitry Malloy, Juan Vazquez, Michael Tang, Omar Cardona, Arti Gupta. 31-45 [doi]
- P4BID: information flow control in p4Karuna Grewal, Loris D'Antoni, Justin Hsu. 46-60 [doi]
- Turning manual concurrent memory reclamation into automatic reference countingDaniel Anderson, Guy E. Blelloch, Yuanhao Wei. 61-75 [doi]
- Low-latency, high-throughput garbage collectionWenyu Zhao, Stephen M. Blackburn, Kathryn S. McKinley. 76-91 [doi]
- Mako: a low-pause, high-throughput evacuating collector for memory-disaggregated datacentersHaoran Ma, Shi Liu, Chenxi Wang, Yifan Qiao, Michael D. Bond, Stephen M. Blackburn, Miryung Kim, Guoqing Harry Xu. 92-107 [doi]
- PaC-trees: supporting parallel and compressed purely-functional collectionsLaxman Dhulipala, Guy E. Blelloch, Yan Gu 0001, Yihan Sun 0001. 108-121 [doi]
- Type-directed program synthesis for RESTful APIsZheng Guo, David Cao, Davin Tjong, Jean Yang 0001, Cole Schlesinger, Nadia Polikarpova. 122-136 [doi]
- Visualization question answering using introspective program synthesisYanju Chen, Xifeng Yan, Yu Feng 0001. 137-151 [doi]
- WebRobot: web robotic process automation using interactive programming-by-demonstrationRui Dong, Zhicheng Huang, Ian Iong Lam, Yan Chen, Xinyu Wang. 152-167 [doi]
- Synthesizing analytical SQL queries from computation demonstrationXiangyu Zhou, Rastislav Bodík, Alvin Cheung, Chenglong Wang. 168-182 [doi]
- Finding typing compiler bugsStefanos Chaliasos, Thodoris Sotiropoulos, Diomidis Spinellis, Arthur Gervais, Benjamin Livshits, Dimitris Mitropoulos. 183-198 [doi]
- IRDL: an IR definition language for SSA compilersMathieu Fehr, Jeff Niu, River Riddle, Mehdi Amini, Zhendong Su 0001, Tobias Grosser. 199-212 [doi]
- Sequential reasoning for optimizing compilers under weak memory concurrencyMinki Cho, Sung Hwan Lee, Dongjae Lee, Chung-Kil Hur, Ori Lahav. 213-228 [doi]
- Can reactive synthesis and syntax-guided synthesis be friends?Wonhyuk Choi, Bernd Finkbeiner, Ruzica Piskac, Mark Santolucito. 229-243 [doi]
- Recursion synthesis with unrealizability witnessesAzadeh Farzan, Danya Lette, Victor Nicolet. 244-259 [doi]
- "Synthesizing input grammars": a replication studyBachir Bendrissou, Rahul Gopinath, Andreas Zeller. 260-268 [doi]
- Autoscheduling for sparse tensor algebra with an asymptotic cost modelPeter Ahrens, Fredrik Kjolstad, Saman P. Amarasinghe. 269-285 [doi]
- DISTAL: the distributed tensor algebra compilerRohan Yadav, Alex Aiken, Fredrik Kjolstad. 286-300 [doi]
- All you need is superword-level parallelism: systematic control-flow vectorization with SLPYishen Chen, Charith Mendis, Saman P. Amarasinghe. 301-315 [doi]
- Warping cache simulation of polyhedral programsCanberk Morelli, Jan Reineke. 316-331 [doi]
- Certified mergeable replicated data typesVimala Soundarapandian, Adharsh Kamath, Kartik Nagar, K. C. Sivaramakrishnan. 332-347 [doi]
- Hamband: RDMA replicated data typesFarzin Houshmand, Javad Saberlatibari, Mohsen Lesani. 348-363 [doi]
- RunTime-assisted convergence in replicated data typesGowtham Kaki, Prasanth Prahladan, Nicholas V. Lewchenko. 364-378 [doi]
- Adore: atomic distributed objects with certified reconfigurationWolf Honoré, Ji-Yong Shin, Jieung Kim, Zhong Shao. 379-394 [doi]
- CycleQ: an efficient basis for cyclic equational reasoningEddie Jones, C.-H. Luke Ong, Steven J. Ramsay. 395-409 [doi]
- Finding the dwarf: recovering precise types from WebAssembly binariesDaniel Lehmann 0002, Michael Pradel. 410-425 [doi]
- Abstract interpretation repairRoberto Bruni, Roberto Giacobazzi, Roberta Gori, Francesco Ranzato. 426-441 [doi]
- Differential cost analysis with simultaneous potentials and anti-potentialsDorde Zikelic, Bor-Yuh Evan Chang, Pauline Bolignano, Franco Raimondi. 442-457 [doi]
- A flexible type system for fearless concurrencyMae Milano, Joshua Turcotti, Andrew C. Myers. 458-473 [doi]
- A study of real-world data races in GolangMilind Chabbi, Murali Krishna Ramanathan. 474-489 [doi]
- Checking robustness to weak persistency modelsHamed Gorjiara, Weiyu Luo, Alex Lee, Guoqing Harry Xu, Brian Demsky. 490-505 [doi]
- Sound sequentialization for concurrent program verificationAzadeh Farzan, Dominik Klumpp, Andreas Podelski. 506-521 [doi]
- Choosing mathematical function implementations for speed and accuracyIan Briggs, Pavel Panchekha. 522-535 [doi]
- Guaranteed bounds for posterior inference in universal probabilistic programmingRaven Beutner, C.-H. Luke Ong, Fabian Zaiser. 536-551 [doi]
- Progressive polynomial approximations for fast correctly rounded math librariesMridul Aanjaneya, Jay P. Lim, Santosh Nagarakatte. 552-565 [doi]
- A typed continuation-passing translation for lexical effect handlersPhilipp Schuster, Jonathan Immanuel Brachthäuser, Marius Müller 0003, Klaus Ostermann. 566-579 [doi]
- Deep and shallow types for gradual languagesBen Greenman. 580-593 [doi]
- Kleene algebra modulo theories: a framework for concrete KATsMichael Greenberg 0002, Ryan Beckett, Eric Hayden Campbell. 594-608 [doi]
- Semantic soundness for language interoperabilityDaniel Patterson 0001, Noble Mushtak, Andrew Wagner, Amal Ahmed. 609-624 [doi]
- Quartz: superoptimization of Quantum circuitsMingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar, Zhihao Jia. 625-640 [doi]
- Giallar: push-button verification for the qiskit Quantum compilerRunzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, Ronghui Gu. 641-656 [doi]
- Algebraic reasoning of Quantum programs via non-idempotent Kleene algebraYuxiang Peng, Mingsheng Ying, Xiaodi Wu. 657-670 [doi]
- PyLSE: a pulse-transfer level language for superconductor electronicsMichael Christensen 0001, Georgios Tzimpragos, Harlan Kringen, Jennifer Volk, Timothy Sherwood, Ben Hardekopf. 671-686 [doi]
- Bind the gap: compiling real software to hardware FFT acceleratorsJackson Woodruff, Jordi Armengol-Estapé, Sam Ainsworth, Michael F. P. O'Boyle. 687-702 [doi]
- Exocompilation for productive programming of hardware acceleratorsYuka Ikarashi, Gilbert Louis Bernstein, Alex Reinking, Hasan Genc, Jonathan Ragan-Kelley. 703-718 [doi]
- PDL: a high-level hardware design language for pipelined processorsDrew Zagieboylo, Charles Sherk, Gookwon Edward Suh, Andrew C. Myers. 719-732 [doi]
- Software-hardware codesign for efficient in-memory regular pattern matchingLingkun Kong, Qixuan Yu, Agnishom Chattopadhyay, Alexis Le Glaunec, Yi Huang, Konstantinos Mamouras, Kaiyuan Yang 0001. 733-748 [doi]
- Deoptless: speculation with dispatched on-stack replacement and specialized continuationsOlivier Flückiger, Jan Jecmen, Sebastián Krynski, Jan Vitek. 749-761 [doi]
- Karp: a language for NP reductionsChenhao Zhang, Jason D. Hartline, Christos Dimoulas. 762-776 [doi]
- WARio: efficient code generation for intermittent computingVito Kortbeek, Souradip Ghosh, Josiah D. Hester, Simone Campanoni, Przemyslaw Pawelczak. 777-791 [doi]
- Compass: strong and compositional library specifications in relaxed memory separation logicHoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer. 792-808 [doi]
- Diaframe: automated verification of fine-grained concurrent programs in IrisIke Mulder, Robbert Krebbers, Herman Geuvers. 809-824 [doi]
- Islaris: verification of machine code against authoritative ISA semanticsMichael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell 0001, Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg 0001, Peter Sewell. 825-840 [doi]
- RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe codeYusuke Matsushita, Xavier Denis, Jacques-Henri Jourdan, Derek Dreyer. 841-856 [doi]
- Efficient approximations for cache-conscious data placementAli Ahmadi, Majid Daliri, Amir Kafshdar Goharshady, Andreas Pavlogiannis. 857-871 [doi]
- FreeTensor: a free-form DSL with holistic optimizations for irregular tensor programsShizhi Tang, Jidong Zhai, Haojie Wang, Lin Jiang, Liyan Zheng, Zhenhao Yuan, Chen Zhang. 872-887 [doi]
- Lasagne: a static binary translator for weak memory model architecturesRodrigo C. O. Rocha, Dennis Sprokholt, Martin Fink, Redha Gouicem, Tom Spink, Soham Chakraborty, Pramod Bhatotia. 888-902 [doi]
- Verifying optimizations of concurrent programs in the promising semanticsJunpeng Zha, Hongjin Liang, Xinyu Feng 0001. 903-917 [doi]
- Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level codeClément Pit-Claudel, Jade Philipoom, Dustin Jamner, Andres Erbsen, Adam Chlipala. 918-933 [doi]
- Formally verified lifting of C-compiled x86-64 binariesFreek Verbeek, Joshua A. Bockenek, Zhoulai Fu, Binoy Ravindran. 934-949 [doi]
- Leapfrog: certified equivalence for protocol parsersRyan Doenges, Tobias Kappé, John Sarracino, Nate Foster, Greg Morrisett. 950-965 [doi]
- Computing correctly with inductive relationsZoe Paraskevopoulou, Aaron Eline, Leonidas Lampropoulos. 966-980 [doi]
- Interpreter-guided differential JIT compiler unit testingGuillermo Polito, Stéphane Ducasse, Pablo Tesone. 981-992 [doi]
- Landmarks and regions: a robust approach to data extractionSuresh Parthasarathy, Lincy Pattanaik, Anirudh Khatry, Arun Shankar Iyer, Arjun Radhakrishna, Sriram K. Rajamani, Mohammad Raza. 993-1009 [doi]
- Odin: on-demand instrumentation with on-the-fly recompilationMingzhe Wang, Jie Liang, Chijin Zhou, Zhiyong Wu, Xinyi Xu, Yu Jiang 0001. 1010-1024 [doi]
- Quickstrom: property-based acceptance testing with LTL specificationsLiam O'Connor, Oskar Wickström. 1025-1038 [doi]