{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T04:50:26Z","timestamp":1773809426552,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":60,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314647","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"802-815","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Abstract interpretation under speculative execution"],"prefix":"10.1145","author":[{"given":"Meng","family":"Wu","sequence":"first","affiliation":[{"name":"Virginia Tech, USA"}]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Southern California, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"2014. Intel\u00ae64 and IA-32 Architectures Optimization Reference Manual. https:\/\/botan.randombit.net\/.  2014. Intel\u00ae64 and IA-32 Architectures Optimization Reference Manual . https:\/\/botan.randombit.net\/."},{"key":"e_1_3_2_2_2_1","unstructured":"2018. LibTomCrypt: A Modular and Portable Cryptographic Toolkit. https:\/\/www.libtom.net\/LibTomCrypt.  2018. LibTomCrypt: A Modular and Portable Cryptographic Toolkit . https:\/\/www.libtom.net\/LibTomCrypt."},{"key":"e_1_3_2_2_3_1","unstructured":"2018. OpenSSH. http:\/\/www.openssh.com\/  2018. OpenSSH. http:\/\/www.openssh.com\/"},{"key":"e_1_3_2_2_4_1","unstructured":"2018. Tesla Motors: Linux. https:\/\/github.com\/teslamotors\/linux.  2018. Tesla Motors: Linux . https:\/\/github.com\/teslamotors\/linux."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062378"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950362"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_8"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2024716.2024718"},{"key":"e_1_3_2_2_9_1","volume-title":"International Conference on Software Engineering. 424-425","author":"Brennan Tegan","year":"2018","unstructured":"Tegan Brennan , Seemanta Saha , and Tevfik Bultan . 2018 . Symbolic path cost analysis for side-channel detection . In International Conference on Software Engineering. 424-425 . Tegan Brennan, Seemanta Saha, and Tevfik Bultan. 2018. Symbolic path cost analysis for side-channel detection. In International Conference on Software Engineering. 424-425."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"crossref","unstructured":"Tevfik Bultan Fang Yu Muath Alkhalaf and Abdulbaki Aydin. 2017. String Analysis for Software Verification and Security.   Tevfik Bultan Fang Yu Muath Alkhalaf and Abdulbaki Aydin. 2017. String Analysis for Software Verification and Security .","DOI":"10.1007\/978-3-319-68670-7"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134058"},{"key":"e_1_3_2_2_12_1","unstructured":"Rapier Chris Steven Michael Bennett Benjamin and Tasota Mike. 2018 (accessed March 1 2019). High Performance SSH\/SCP - HPN-SSH. https:\/\/www.psc.edu\/hpn-ssh  Rapier Chris Steven Michael Bennett Benjamin and Tasota Mike. 2018 (accessed March 1 2019). High Performance SSH\/SCP - HPN-SSH. https:\/\/www.psc.edu\/hpn-ssh"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2016.7461358"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_2_16_1","volume-title":"USENIX Security Symposium. 431-446","author":"Doychev Goran","year":"2013","unstructured":"Goran Doychev , Dominik Feld , Boris K\u00f6pf , Laurent Mauborgne , and Jan Reineke . 2013 . CacheAudit: A tool for the static analysis of cache side channels . In USENIX Security Symposium. 431-446 . Goran Doychev, Dominik Feld, Boris K\u00f6pf, Laurent Mauborgne, and Jan Reineke. 2013. CacheAudit: A tool for the static analysis of cache side channels. In USENIX Security Symposium. 431-446."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2685616"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00010-6"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/646905.710485"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008186323068"},{"key":"e_1_3_2_2_21_1","volume-title":"The Effect of the Speculation Depth on the Performance of Superscalar Architectures. In International Euro-Par Conference on Parallel Processing. 1061-1065","author":"Eliseu","unstructured":"Eliseu M. Chaves Filho and Edil S. Tavares Fernandes. 1997 . The Effect of the Speculation Depth on the Performance of Superscalar Architectures. In International Euro-Par Conference on Parallel Processing. 1061-1065 . Eliseu M. Chaves Filho and Edil S. Tavares Fernandes. 1997. The Effect of the Speculation Depth on the Performance of Superscalar Architectures. In International Euro-Par Conference on Parallel Processing. 1061-1065."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303976"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s13389-016-0141-6"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236028"},{"key":"e_1_3_2_2_25_1","volume-title":"Present and Future. In International Workshop on Worst-Case Execution Time Analysis. 137- 147","author":"Gustafsson Jan","year":"2010","unstructured":"Jan Gustafsson , Adam Betts , Andreas Ermedahl , and Bj\u00f6rn Lisper . 2010 . The M\u00e4lardalen WCET Benchmarks - Past , Present and Future. In International Workshop on Worst-Case Execution Time Analysis. 137- 147 . Jan Gustafsson, Adam Betts, Andreas Ermedahl, and Bj\u00f6rn Lisper. 2010. The M\u00e4lardalen WCET Benchmarks - Past, Present and Future. In International Workshop on Worst-Case Execution Time Analysis. 137- 147."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/WWC.2001.990739"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/580550.876441"},{"key":"e_1_3_2_2_28_1","volume-title":"Spectre Attacks: Exploiting Speculative Execution. ArXiv e-prints (Jan.","author":"Kocher Paul","year":"2018","unstructured":"Paul Kocher , Daniel Genkin , Daniel Gruss , Werner Haas , Mike Hamburg , Moritz Lipp , Stefan Mangard , Thomas Prescher , Michael Schwarz , and Yuval Yarom . 2018 . Spectre Attacks: Exploiting Speculative Execution. ArXiv e-prints (Jan. 2018). arXiv:1801.01203 Paul Kocher, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. 2018. Spectre Attacks: Exploiting Speculative Execution. ArXiv e-prints (Jan. 2018). arXiv:1801.01203"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_40"},{"key":"e_1_3_2_2_30_1","volume-title":"Flow-Sensitive Composition of Thread-Modular Abstract Interpretation. In ACM SIGSOFT Symposium on Foundations of Software Engineering.","author":"Kusano Markus","year":"2016","unstructured":"Markus Kusano and Chao Wang . 2016 . Flow-Sensitive Composition of Thread-Modular Abstract Interpretation. In ACM SIGSOFT Symposium on Foundations of Software Engineering. Markus Kusano and Chao Wang. 2016. Flow-Sensitive Composition of Thread-Modular Abstract Interpretation. In ACM SIGSOFT Symposium on Foundations of Software Engineering."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106243"},{"key":"e_1_3_2_2_32_1","volume-title":"LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In IEEE \/ ACM International Symposium on Code Generation and Optimization. 75-88","author":"Lattner Chris","unstructured":"Chris Lattner and Vikram S. Adve . 2004 . LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In IEEE \/ ACM International Symposium on Code Generation and Optimization. 75-88 . Chris Lattner and Vikram S. Adve. 2004. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In IEEE \/ ACM International Symposium on Code Generation and Optimization. 75-88."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775953"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11241-006-9205-5"},{"key":"e_1_3_2_2_35_1","volume-title":"Timing Analysis of Concurrent Programs Running on Shared Cache Multi-Cores. In IEEE Real-Time Systems Symposium. 57-67","author":"Li Yan","year":"2009","unstructured":"Yan Li , Vivy Suhendra , Yun Liang , Tulika Mitra , and Abhik Roychoudhury . 2009 . Timing Analysis of Concurrent Programs Running on Shared Cache Multi-Cores. In IEEE Real-Time Systems Symposium. 57-67 . Yan Li, Vivy Suhendra, Yun Liang, Tulika Mitra, and Abhik Roychoudhury. 2009. Timing Analysis of Concurrent Programs Running on Shared Cache Multi-Cores. In IEEE Real-Time Systems Symposium. 57-67."},{"key":"e_1_3_2_2_36_1","volume-title":"ArXiv e-prints (Jan","author":"Lipp Moritz","year":"2018","unstructured":"Moritz Lipp , Michael Schwarz , Daniel Gruss , Thomas Prescher , Werner Haas , Stefan Mangard , Paul Kocher , Daniel Genkin , Yuval Yarom , and Mike Hamburg . 2018. Meltdown. ArXiv e-prints (Jan . 2018 ). arXiv:1801.01207 Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, and Mike Hamburg. 2018. Meltdown. ArXiv e-prints (Jan. 2018). arXiv:1801.01207"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2010.30"},{"key":"e_1_3_2_2_38_1","volume-title":"Trace Partitioning in Abstract Interpretation Based Static Analyzers. In European Symposium on Programming Languages and Systems. 5-20","author":"Mauborgne Laurent","year":"2005","unstructured":"Laurent Mauborgne and Xavier Rival . 2005 . Trace Partitioning in Abstract Interpretation Based Static Analyzers. In European Symposium on Programming Languages and Systems. 5-20 . Laurent Mauborgne and Xavier Rival. 2005. Trace Partitioning in Abstract Interpretation Based Static Analyzers. In European Symposium on Programming Languages and Systems. 5-20."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2907950.2907961"},{"key":"e_1_3_2_2_40_1","volume-title":"The octagon abstract domain. Higher-order and symbolic computation 19, 1","author":"Min\u00e9 Antoine","year":"2006","unstructured":"Antoine Min\u00e9 . 2006. The octagon abstract domain. Higher-order and symbolic computation 19, 1 ( 2006 ), 31-100. Antoine Min\u00e9. 2006. The octagon abstract domain. Higher-order and symbolic computation 19, 1 (2006), 31-100."},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/MDAT.2018.2794204"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"crossref","unstructured":"F Nielson Riis H Nielson and CL Hankin. 1999. Principles of Program Analysis. (1999).   F Nielson Riis H Nielson and CL Hankin. 1999. Principles of Program Analysis. (1999).","DOI":"10.1007\/978-3-662-03811-6"},{"key":"e_1_3_2_2_43_1","volume-title":"Multi-run Side-Channel Analysis Using Symbolic Execution and Max-SMT. In IEEE Computer Security Foundations Symposium. 387-400","author":"Pasareanu Corina S.","year":"2016","unstructured":"Corina S. Pasareanu , Quoc-Sang Phan , and Pasquale Malacaria . 2016 . Multi-run Side-Channel Analysis Using Symbolic Execution and Max-SMT. In IEEE Computer Security Foundations Symposium. 387-400 . Corina S. Pasareanu, Quoc-Sang Phan, and Pasquale Malacaria. 2016. Multi-run Side-Channel Analysis Using Symbolic Execution and Max-SMT. In IEEE Computer Security Foundations Symposium. 387-400."},{"key":"e_1_3_2_2_44_1","volume-title":"Synthesis of Adaptive Side-Channel Attacks. In IEEE Computer Security Foundations Symposium. 328-342","author":"Phan Quoc-Sang","year":"2017","unstructured":"Quoc-Sang Phan , Lucas Bang , Corina S. Pasareanu , Pasquale Malacaria , and Tevfik Bultan . 2017 . Synthesis of Adaptive Side-Channel Attacks. In IEEE Computer Security Foundations Symposium. 328-342 . Quoc-Sang Phan, Lucas Bang, Corina S. Pasareanu, Pasquale Malacaria, and Tevfik Bultan. 2017. Synthesis of Adaptive Side-Channel Attacks. In IEEE Computer Security Foundations Symposium. 328-342."},{"key":"e_1_3_2_2_45_1","volume-title":"The Effect of Speculative Execution on Cache Performance. In International Symposium on Parallel Processing. 172-179","author":"Pierce Jim","unstructured":"Jim Pierce and Trevor N. Mudge . 1994 . The Effect of Speculative Execution on Cache Performance. In International Symposium on Parallel Processing. 172-179 . Jim Pierce and Trevor N. Mudge. 1994. The Effect of Speculative Execution on Cache Performance. In International Symposium on Parallel Processing. 172-179."},{"key":"e_1_3_2_2_46_1","volume-title":"Statische pipeline-analyse f\u00fcr echtzeitsysteme. Dipl. thesis","author":"Schneider J\u00f6rn","year":"1998","unstructured":"J\u00f6rn Schneider . 1998. Statische pipeline-analyse f\u00fcr echtzeitsysteme. Dipl. thesis , Univ. Saarland , Saarbruecken, Germany ( 1998 ). J\u00f6rn Schneider. 1998. Statische pipeline-analyse f\u00fcr echtzeitsysteme. Dipl. thesis, Univ. Saarland, Saarbruecken, Germany (1998)."},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/315253.314432"},{"key":"e_1_3_2_2_48_1","volume-title":"ACM\/IEEE International conference on Embedded Software. 203-212","author":"Sen Rathijit","unstructured":"Rathijit Sen and Y. N. Srikant . 2007. WCET estimation for executables in the presence of data caches . In ACM\/IEEE International conference on Embedded Software. 203-212 . Rathijit Sen and Y. N. Srikant. 2007. WCET estimation for executables in the presence of data caches. In ACM\/IEEE International conference on Embedded Software. 203-212."},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/3155562.3155592"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3240485"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008141130870"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.111.0025"},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_2"},{"key":"e_1_3_2_2_55_1","volume-title":"USENIX Security Symposium.","author":"Bulck Jo Van","year":"2018","unstructured":"Jo Van Bulck , Marina Minkin , Ofir Weisse , Daniel Genkin , Baris Kasikci , Frank Piessens , Mark Silberstein , Thomas F. Wenisch , Yuval Yarom , and Raoul Strackx . 2018 . Foreshadow: Extracting the Keys to the Intel SGX Kingdom with Transient Out-of-Order Execution . In USENIX Security Symposium. Jo Van Bulck, Marina Minkin, Ofir Weisse, Daniel Genkin, Baris Kasikci, Frank Piessens, Mark Silberstein, Thomas F. Wenisch, Yuval Yarom, and Raoul Strackx. 2018. Foreshadow: Extracting the Keys to the Intel SGX Kingdom with Transient Out-of-Order Execution. In USENIX Security Symposium."},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/IJCNN.1999.831066"},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_3"},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213851"},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/123465.123475"},{"key":"e_1_3_2_2_60_1","volume-title":"SCInfer: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks. In International Conference on Computer Aided Verification. 157-177","author":"Zhang Jun","year":"2018","unstructured":"Jun Zhang , Pengfei Gao , Fu Song , and Chao Wang . 2018 . SCInfer: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks. In International Conference on Computer Aided Verification. 157-177 . Jun Zhang, Pengfei Gao, Fu Song, and Chao Wang. 2018. SCInfer: Refinement-Based Verification of Software Countermeasures Against Side-Channel Attacks. In International Conference on Computer Aided Verification. 157-177."}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314647","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314647","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:29Z","timestamp":1750204409000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314647"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":60,"alternative-id":["10.1145\/3314221.3314647","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314647","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}