{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:39:45Z","timestamp":1773193185154,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":53,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,3,30]],"date-time":"2025-03-30T00:00:00Z","timestamp":1743292800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100006374","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CNS-1954521,CNS-1942888,CNS-2154183,CCF-8191902"],"award-info":[{"award-number":["CNS-1954521,CNS-1942888,CNS-2154183,CCF-8191902"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,3,30]]},"DOI":"10.1145\/3669940.3707263","type":"proceedings-article","created":{"date-parts":[[2025,2,6]],"date-time":"2025-02-06T12:28:01Z","timestamp":1738844881000},"page":"603-618","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["H-H\n            <scp>oudini<\/scp>\n            : Scalable Invariant Learning"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-6685-7226","authenticated-orcid":false,"given":"Sushant","family":"Dinesh","sequence":"first","affiliation":[{"name":"University of California, Berkeley, Berkeley, California, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6191-8187","authenticated-orcid":false,"given":"Yongye","family":"Zhu","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, California, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9995-5995","authenticated-orcid":false,"given":"Christopher W.","family":"Fletcher","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Berkeley, California, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,3,30]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"ChaCha20 (BearSSL). https:\/\/bearssl.org\/gitweb\/. Accessed: 2024-12-14."},{"key":"e_1_3_2_1_2_1","volume-title":"FMCAD'13","author":"Alur Rajeev","unstructured":"Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In FMCAD'13."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2020.2996616"},{"key":"e_1_3_2_1_4_1","unstructured":"Anyscale. Anyscale homepage. https:\/\/www.anyscale.com\/. Accessed: 2024-06-23."},{"key":"e_1_3_2_1_5_1","unstructured":"Krste Asanovi\u0107 Rimas Avizienis Jonathan Bachrach Scott Beamer David Biancolin Christopher Celio Henry Cook Daniel Dabbelt John Hauser Adam Izraelevitz Sagar Karandikar Ben Keller Donggyu Kim John Koenig Yunsup Lee Eric Love Martin Maas Albert Magyar Howard Mao Miquel Moreto Albert Ou David A. Patterson Brian Richards Colin Schmidt Stephen Twigg Huy Vo and Andrew Waterman. The Rocket Chip Generator. Technical Report UCB\/EECS-2016-17 EECS Department University of California Berkeley 2016."},{"key":"e_1_3_2_1_6_1","unstructured":"Thomas Ball Rupak Majumdar Todd D. Millstein and Sriram K. Rajamani. Automatic predicate abstraction of C programs. In PLDI'01."},{"key":"e_1_3_2_1_7_1","unstructured":"Daniel J. Bernstein. djbsort. https:\/\/sorting.cr.yp.to\/. Accessed: 2024-12-14."},{"key":"e_1_3_2_1_8_1","volume-title":"VMCAI'11","author":"Bradley Aaron R","unstructured":"Aaron R Bradley. SAT-based model checking without unrolling. In VMCAI'11."},{"key":"e_1_3_2_1_9_1","unstructured":"Cristiano Calcagno Dino Distefano Peter O'Hearn and Hongseok Yang. Compositional shape analysis by means of bi-abduction. In POPL'09."},{"key":"e_1_3_2_1_10_1","volume-title":"APLAS'09","author":"Calcagno Cristiano","unstructured":"Cristiano Calcagno, Dino Distefano, and Viktor Vafeiadis. Bi-abductive resource invariant synthesis. In APLAS'09."},{"key":"e_1_3_2_1_11_1","unstructured":"Sunjay Cauligi Gary Soeller Brian Johannesmeyer Fraser Brown Riad S. Wahby John Renner Benjamin Gr\u00e9goire Gilles Barthe Ranjit Jhala and Deian Stefan. FaCT: A DSL for Timing-Sensitive Computation. In PLDI'19."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09571-y"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0257-4"},{"key":"e_1_3_2_1_14_1","unstructured":"Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL'77."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.2307\/2963593"},{"key":"e_1_3_2_1_16_1","volume-title":"DAC'22","author":"Deutschmann Lucas","unstructured":"Lucas Deutschmann, Johannes M\u00fcller, Mohammad R. Fadiheh, Dominik Stoffel, and Wolfgang Kunz. Towards a Formally Verified Hardware Root-of-Trust for Data-Oblivious Computing. In DAC'22."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2024.3374249"},{"key":"e_1_3_2_1_18_1","volume-title":"OOPSLA'13","author":"Dillig Isil","unstructured":"Isil Dillig, Thomas Dillig, Boyang Li, and Kenneth L. McMillan. Inductive invariant generation via abductive inference. In OOPSLA'13."},{"key":"e_1_3_2_1_19_1","volume-title":"Fletcher. SynthCT: Towards Portable Constant-Time Code. In NDSS'22","author":"Dinesh Sushant","unstructured":"Sushant Dinesh, Grant Garrett-Grossman, and Christopher W. Fletcher. SynthCT: Towards Portable Constant-Time Code. In NDSS'22."},{"key":"e_1_3_2_1_20_1","unstructured":"Sushant Dinesh Madhusudan Parthasarathy and Christopher Fletcher. CONJUNCT: Learning inductive invariants to prove unbounded instruction safety against microarchitectural timing attacks. In S&P'24."},{"key":"e_1_3_2_1_21_1","volume-title":"Fletcher","author":"Dinesh Sushant","year":"2024","unstructured":"Sushant Dinesh, Yongye Zhu, and Christopher W. Fletcher. VeloCT. https:\/\/github.com\/FPSG-UIUC\/veloct. Accessed: 2024-12-15."},{"key":"e_1_3_2_1_22_1","volume-title":"FMCAD'11","author":"E\u00e9n Niklas","unstructured":"Niklas E\u00e9n, Alan Mishchenko, and Robert Brayton. Efficient implementation of property directed reachability. In FMCAD'11."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337240"},{"key":"e_1_3_2_1_24_1","volume-title":"OOPSLA'18","author":"Ezudheen P.","unstructured":"P. Ezudheen, Daniel Neider, Deepak D'Souza, Pranav Garg, and P. Madhusudan. Horn-ICE learning for synthesizing invariants and contracts. In OOPSLA'18."},{"key":"e_1_3_2_1_25_1","unstructured":"Mohammad Rahmani Fadiheh Dominik Stoffel Clark W. Barrett Subhasish Mitra and Wolfgang Kunz. Processor hardware security vulnerabilities and their detection by unique program execution checking. In DATE'19."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2022.3152666"},{"key":"e_1_3_2_1_27_1","volume-title":"FMCAD'17","author":"Fedyukovich Grigory","unstructured":"Grigory Fedyukovich, Samuel J Kaufman, and Rastislav Bod\u00edk. Sampling invariants from frequency distributions. In FMCAD'17."},{"key":"e_1_3_2_1_28_1","volume-title":"FME'01","author":"Flanagan Cormac","unstructured":"Cormac Flanagan and K Rustan M Leino. Houdini, an annotation assistant for ESC\/Java. In FME'01."},{"key":"e_1_3_2_1_29_1","volume-title":"ASPLOS'14","author":"Flanders Michael","unstructured":"Michael Flanders, Reshabh K. Sharma, Alexandra E. Michael, Dan Grossman, and David Kohlbrenner. Avoiding instruction-centric microarchitectural timing channels via binary-code transformations. In ASPLOS'14."},{"key":"e_1_3_2_1_30_1","volume-title":"CAV'14","author":"Garg Pranav","unstructured":"Pranav Garg, Christof L\u00f6ding, Parthasarathy Madhusudan, and Daniel Neider. ICE: A robust framework for learning invariants. In CAV'14."},{"key":"e_1_3_2_1_31_1","volume-title":"ILPS'94","author":"Giacobazzi Roberto","unstructured":"Roberto Giacobazzi. Abductive analysis of modular logic programs. In ILPS'94."},{"key":"e_1_3_2_1_32_1","volume-title":"TACAS'20","author":"Goel Aman","unstructured":"Aman Goel and Karem A. Sakallah. AVR: abstractly verifying reachability. In TACAS'20."},{"key":"e_1_3_2_1_33_1","unstructured":"Sumit Gulwani Saurabh Srivastava and Ramarathnam Venkatesan. Program analysis as constraint solving. In PLDI'08."},{"key":"e_1_3_2_1_34_1","volume-title":"FMCAD'15","author":"Ivrii Alexander","unstructured":"Alexander Ivrii and Arie Gurfinkel. Pushing to the top. In FMCAD'15."},{"key":"e_1_3_2_1_35_1","volume-title":"ISCA '17","author":"Jouppi Norman P.","unstructured":"Norman P. Jouppi, Cliff Young, Nishant Patil, David Patterson, Gaurav Agrawal, Raminder Bajwa, Sarah Bates, Suresh Bhatia, Nan Boden, Al Borchers, Rick Boyle, Pierre-luc Cantin, Clifford Chao, Chris Clark, Jeremy Coriell, Mike Daley, Matt Dau, Jeffrey Dean, Ben Gelb, Tara Vazir Ghaemmaghami, Rajendra Gottipati, William Gulland, Robert Hagmann, C. Richard Ho, Doug Hogberg, John Hu, Robert Hundt, Dan Hurt, Julian Ibarz, Aaron Jaffey, Alek Jaworski, Alexander Kaplan, Harshit Khaitan, Daniel Killebrew, Andy Koch, Naveen Kumar, Steve Lacy, James Laudon, James Law, Diemthu Le, Chris Leary, Zhuyuan Liu, Kyle Lucke, Alan Lundin, Gordon MacKean, Adriana Maggiore, Maire Mahony, Kieran Miller, Rahul Nagarajan, Ravi Narayanaswami, Ray Ni, Kathy Nix, Thomas Norrie, Mark Omernick, Narayana Penukonda, Andy Phelps, Jonathan Ross, Matt Ross, Amir Salek, Emad Samadiani, Chris Severn, Gregory Sizikov, Matthew Snelham, Jed Souter, Dan Steinberg, Andy Swing, Mercedes Tan, Gregory Thorson, Bo Tian, Horia Toma, Erick Tuttle, Vijay Vasudevan, Richard Walter, Walter Wang, Eric Wilcox, and Doe Hyun Yoon. In-datacenter performance analysis of a tensor processing unit. In ISCA '17."},{"key":"e_1_3_2_1_36_1","unstructured":"Paul Kocher Daniel Genkin Daniel Gruss Werner Haas Mike Hamburg Moritz Lipp Stefan Mangard Thomas Prescher Michael Schwarz and Yuval Yarom. Spectre Attacks: Exploiting Speculative Execution. In S&P'19."},{"key":"e_1_3_2_1_37_1","volume-title":"CRYPTO'96","author":"Kocher Paul C.","unstructured":"Paul C. Kocher. Timing Attacks on Implementations of Diffie-Hellman, RSA, DSS, and Other Systems. In CRYPTO'96."},{"key":"e_1_3_2_1_38_1","unstructured":"Moritz Lipp Michael Schwarz Daniel Gruss Thomas Prescher Werner Haas Stefan Mangard Paul Kocher Daniel Genkin Yuval Yarom and Mike Hamburg. Meltdown: Reading Kernel Memory from User Space. In USENIX Security'18."},{"key":"e_1_3_2_1_39_1","volume-title":"CAV'03","author":"McMillan Kenneth L.","unstructured":"Kenneth L. McMillan. Interpolation and SAT-based model checking. In CAV'03."},{"key":"e_1_3_2_1_40_1","volume-title":"SORCAR: Property-Driven Algorithms for Learning Conjunctive Invariants. In SAS'19","author":"Neider Daniel","unstructured":"Daniel Neider, Shambwaditya Saha, Pranav Garg, and P. Madhusudan. SORCAR: Property-Driven Algorithms for Learning Conjunctive Invariants. In SAS'19."},{"key":"e_1_3_2_1_41_1","volume-title":"CAV'18","author":"Niemetz Aina","unstructured":"Aina Niemetz, Mathias Preiner, Clifford Wolf, and Armin Biere. Btor2, btormc and boolector 3.0. In CAV'18."},{"key":"e_1_3_2_1_42_1","volume-title":"Collected papers of charles sanders peirce","author":"Peirce Charles Sanders","year":"1974","unstructured":"Charles Sanders Peirce. Collected papers of charles sanders peirce, volume 5. Harvard University Press, 1974."},{"key":"e_1_3_2_1_43_1","unstructured":"Armando Solar-Lezama. Program synthesis by sketching. PhD thesis USA 2008."},{"key":"e_1_3_2_1_44_1","volume-title":"ASPLOS'06","author":"Solar-Lezama Armando","unstructured":"Armando Solar-Lezama, Liviu Tancau, Rastislav Bod\u00edk, Sanjit A. Seshia, and Vijay A. Saraswat. Combinatorial sketching for finite programs. In ASPLOS'06."},{"key":"e_1_3_2_1_45_1","unstructured":"Qinhan Tan Yuheng Yang Thomas Bourgeat Sharad Malik and Mengjia Yan. RTL verification for secure speculation using contract shadow logic. In Arxiv'24."},{"key":"e_1_3_2_1_46_1","unstructured":"Klaus v. Gleissenthall Rami G\u00f6khan K\u0131c\u0131 Deian Stefan and Ranjit Jhala. IODINE: Verifying Constant-Time Execution of Hardware. In USENIX Security'19."},{"key":"e_1_3_2_1_47_1","volume-title":"CCS'21","author":"Gleissenthall Klaus V.","unstructured":"Klaus V. Gleissenthall, Rami G\u00f6khan K\u0131c\u0131, Deian Stefan, and Ranjit Jhala. Solver-aided constant-time hardware verification. In CCS'21."},{"key":"e_1_3_2_1_48_1","volume-title":"ICE. In VMCAI'17","author":"Vizel Yakir","unstructured":"Yakir Vizel, Arie Gurfinkel, Sharon Shoham, and Sharad Malik. IC3- flipping the E in ICE. In VMCAI'17."},{"key":"e_1_3_2_1_49_1","volume-title":"CCS'23","author":"Wang Zilong","unstructured":"Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, and Marco Guarnieri. Specification and verification of side-channel security for open-source processors via leakage contracts. In CCS'23."},{"key":"e_1_3_2_1_50_1","unstructured":"Claire Wolf. Yosys Open SYnthesis Suite. https:\/\/yosyshq.net\/yosys\/. Accessed: 2024-12-14."},{"key":"e_1_3_2_1_51_1","volume-title":"Fletcher. Data Oblivious ISA Extensions for Side Channel-Resistant and High Performance Computing. In NDSS'19","author":"Yu Jiyong","unstructured":"Jiyong Yu, Lucas Hsiung, Mohamad El Hajj, and Christopher W. Fletcher. Data Oblivious ISA Extensions for Side Channel-Resistant and High Performance Computing. In NDSS'19."},{"key":"e_1_3_2_1_52_1","volume-title":"Sonicboom: The 3rd generation berkeley out-of-order machine","author":"Zhao Jerry","year":"2020","unstructured":"Jerry Zhao, Ben Korpan, Abraham Gonzalez, and Krste Asanovic. Sonicboom: The 3rd generation berkeley out-of-order machine. May 2020."},{"key":"e_1_3_2_1_53_1","unstructured":"He Zhu Stephen Magill and Suresh Jagannathan. A data-driven CHC solver. In PLDI'18."}],"event":{"name":"ASPLOS '25: 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","location":"Rotterdam Netherlands","acronym":"ASPLOS '25","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGOPS ACM Special Interest Group on Operating Systems","SIGARCH ACM Special Interest Group on Computer Architecture"]},"container-title":["Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3669940.3707263","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3669940.3707263","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T14:45:59Z","timestamp":1755787559000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3669940.3707263"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,30]]},"references-count":53,"alternative-id":["10.1145\/3669940.3707263","10.1145\/3669940"],"URL":"https:\/\/doi.org\/10.1145\/3669940.3707263","relation":{},"subject":[],"published":{"date-parts":[[2025,3,30]]},"assertion":[{"value":"2025-03-30","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}