{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T11:02:29Z","timestamp":1750503749828,"version":"3.37.3"},"reference-count":21,"publisher":"IEEE","license":[{"start":{"date-parts":[[2021,11,1]],"date-time":"2021-11-01T00:00:00Z","timestamp":1635724800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2021,11,1]],"date-time":"2021-11-01T00:00:00Z","timestamp":1635724800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["VRG11-005"],"award-info":[{"award-number":["VRG11-005"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,11,1]]},"DOI":"10.1109\/iccad51958.2021.9643462","type":"proceedings-article","created":{"date-parts":[[2021,12,23]],"date-time":"2021-12-23T23:06:46Z","timestamp":1640300806000},"page":"1-9","source":"Crossref","is-referenced-by-count":3,"title":["Bounded Model Checking of Speculative Non-Interference"],"prefix":"10.1109","author":[{"given":"Emmanuel","family":"Pescosta","sequence":"first","affiliation":[{"name":"TU Wien,Vienna,Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[{"name":"TU Wien,Vienna,Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[{"name":"TU Wien,Vienna,Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"journal-title":"The SMT-LIB Standard Version 2 6","year":"2017","author":"barrett","key":"ref11"},{"journal-title":"SPEcBMC implementation","year":"0","author":"pescosta","key":"ref12"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00027"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_29"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/2756550"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134058"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_11"},{"key":"ref19","first-page":"158","article-title":"Automating modular verification of secure information flow","author":"pick","year":"2020","journal-title":"Formal Methods in Computer-Aided Design (FMCAD)"},{"journal-title":"Spectre mitigations in MSVC","year":"0","author":"pardoe","key":"ref4"},{"key":"ref3","first-page":"249","article-title":"A systematic evaluation of transient execution attacks and defenses","author":"canella","year":"2019","journal-title":"USENIX Security Symposium"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"journal-title":"Spectre Mitigations in Microsoft's C\/C++ Compiler","year":"0","author":"kocher","key":"ref5"},{"key":"ref8","first-page":"156","article-title":"The program counter security model: Automatic detection and removal of control-flow side channel attacks","volume":"3935","author":"molnar","year":"2005","journal-title":"Information Security and Cryptology (ICISC) '02 LNCS"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00011"},{"key":"ref2","article-title":"Spectre is here to stay: An analysis of side-channels and speculative execution","volume":"abs 1902 5178","author":"mcilroy","year":"2019","journal-title":"The Computing Research Repository"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/3399742"},{"journal-title":"SpecBMC Bounded model checker for speculative non-interference","year":"2020","author":"pescosta","key":"ref9"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240844"},{"key":"ref21","first-page":"377","article-title":"MASCAT: preventing micro architectural attacks before distribution","author":"irazoqui","year":"2018","journal-title":"Conference on Data and Applications Security and Privacy"}],"event":{"name":"2021 IEEE\/ACM International Conference On Computer Aided Design (ICCAD)","start":{"date-parts":[[2021,11,1]]},"location":"Munich, Germany","end":{"date-parts":[[2021,11,4]]}},"container-title":["2021 IEEE\/ACM International Conference On Computer Aided Design (ICCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9643423\/9643432\/09643462.pdf?arnumber=9643462","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T21:32:02Z","timestamp":1667511122000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9643462\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,1]]},"references-count":21,"URL":"https:\/\/doi.org\/10.1109\/iccad51958.2021.9643462","relation":{},"subject":[],"published":{"date-parts":[[2021,11,1]]}}}