{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:51:24Z","timestamp":1760043084874,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,1,20]],"date-time":"2020-01-20T00:00:00Z","timestamp":1579478400000},"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":[[2020,1,20]]},"DOI":"10.1145\/3372885.3373811","type":"proceedings-article","created":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T13:09:33Z","timestamp":1579698573000},"page":"47-60","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Verifying x86 instruction implementations"],"prefix":"10.1145","author":[{"given":"Shilpi","family":"Goel","sequence":"first","affiliation":[{"name":"Centaur Technology, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anna","family":"Slobodova","sequence":"additional","affiliation":[{"name":"Centaur Technology, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rob","family":"Sumners","sequence":"additional","affiliation":[{"name":"Centaur Technology, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sol","family":"Swords","sequence":"additional","affiliation":[{"name":"Centaur Technology, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,1,22]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"December","author":"Accessed","year":"2019","unstructured":"Accessed : December 2019 . ACL2 Books : Codewalker. Online . https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/projects\/ codewalker . Accessed: December 2019. ACL2 Books: Codewalker. Online. https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/projects\/ codewalker ."},{"key":"e_1_3_2_1_2_1","volume-title":"December","author":"Accessed","year":"2019","unstructured":"Accessed : December 2019 . ACL2 Home Page. Online . http:\/\/www.cs.utexas.edu\/users\/moore\/acl2 . Accessed: December 2019. ACL2 Home Page. Online. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2 ."},{"key":"e_1_3_2_1_3_1","volume-title":"December","author":"Accessed","year":"2019","unstructured":"Accessed : December 2019 . Documentation of SV: A Hardware Verification Library . Online. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/ manual\/?topic=ACL2____SV . Accessed: December 2019. Documentation of SV: A Hardware Verification Library. Online. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/ manual\/?topic=ACL2____SV ."},{"key":"e_1_3_2_1_4_1","volume-title":"December","author":"Accessed","year":"2019","unstructured":"Accessed : December 2019 . Documentation of VL Verilog Toolkit. Online . http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/ manual\/?topic=ACL2____VL . Accessed: December 2019. Documentation of VL Verilog Toolkit. Online. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/ manual\/?topic=ACL2____VL ."},{"key":"e_1_3_2_1_5_1","volume-title":"December","author":"Accessed","year":"2019","unstructured":"Accessed : December 2019 . SV : A Hardware Verification Library . Online. https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/centaur\/sv . Accessed: December 2019. SV: A Hardware Verification Library. Online. https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/centaur\/sv ."},{"key":"e_1_3_2_1_6_1","volume-title":"December","author":"Accessed","year":"2019","unstructured":"Accessed : December 2019 . SVTV : A Structure for Simulation Pattern of a Hardware Design. Online . http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/ manual\/?topic=ACL2____DEFSVTV . Accessed: December 2019. SVTV: A Structure for Simulation Pattern of a Hardware Design. Online. http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/manuals\/current\/ manual\/?topic=ACL2____DEFSVTV ."},{"key":"e_1_3_2_1_7_1","volume-title":"December","author":"Accessed","year":"2019","unstructured":"Accessed : December 2019 . VL Verilog Toolkit. Online . https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/centaur\/vl . Accessed: December 2019. VL Verilog Toolkit. Online. https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/centaur\/vl ."},{"key":"e_1_3_2_1_8_1","volume-title":"December","author":"Accessed","year":"2019","unstructured":"Accessed : December 2019 . x86isa Library in the ACL2 Community Books . Online. https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/projects\/x86isa . Accessed: December 2019. x86isa Library in the ACL2 Community Books. Online. https:\/\/github.com\/acl2\/acl2\/tree\/master\/books\/projects\/x86isa ."},{"volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"Hunt Warren A.","key":"e_1_3_2_1_9_1","unstructured":"Warren A. Hunt Jr ., Sol Swords , Jared Davis , and Anna Slobodova . 2010. Use of Formal Verification at Centaur Technology . In Design and Verification of Microprocessor Systems for High-Assurance Applications , David Hardin (Ed.). Springer , 65\u201388. Warren A. Hunt Jr., Sol Swords, Jared Davis, and Anna Slobodova. 2010. Use of Formal Verification at Centaur Technology. In Design and Verification of Microprocessor Systems for High-Assurance Applications, David Hardin (Ed.). Springer, 65\u201388."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_8"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-X_17"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/277044.277189"},{"volume-title":"Proceedings 1999 Design Automation Conference (Cat. No. 99CH36361)","author":"Aagaard Mark D.","key":"e_1_3_2_1_13_1","unstructured":"Mark D. Aagaard , Robert B. Jones , and Carl-Johan H. Seger . 1999. Formal verification using parametric representations of Boolean constraints . In Proceedings 1999 Design Automation Conference (Cat. No. 99CH36361) . IEEE, 402\u2013407. Mark D. Aagaard, Robert B. Jones, and Carl-Johan H. Seger. 1999. Formal verification using parametric representations of Boolean constraints. In Proceedings 1999 Design Automation Conference (Cat. No. 99CH36361). IEEE, 402\u2013407."},{"volume-title":"Proceedings of the 9th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE). IEEE\/ACM","author":"Slobodova Anna","key":"e_1_3_2_1_14_1","unstructured":"Anna Slobodova , Jared Davis , Sol Swords , and Warren A . Hunt Jr. 2011. A flexible formal verification framework for industrial scale validation . In Proceedings of the 9th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE). IEEE\/ACM , Cambridge, UK, 89\u201397. Anna Slobodova, Jared Davis, Sol Swords, and Warren A. Hunt Jr. 2011. A flexible formal verification framework for industrial scale validation. In Proceedings of the 9th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE). IEEE\/ACM, Cambridge, UK, 89\u201397."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_20"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.280.6"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_1"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/1998496.1998520"},{"volume-title":"Proceedings of the 21st International Conference on Computer Aided Verification (CAV). 353\u2013367","author":"Hunt Warren A.","key":"e_1_3_2_1_19_1","unstructured":"Warren A. Hunt Jr . and Sol Swords. 2009. Centaur Technology media unit verification . In Proceedings of the 21st International Conference on Computer Aided Verification (CAV). 353\u2013367 . Warren A. Hunt Jr. and Sol Swords. 2009. Centaur Technology media unit verification. In Proceedings of the 21st International Conference on Computer Aided Verification (CAV). 353\u2013367."},{"key":"e_1_3_2_1_20_1","unstructured":"Intel Corporation. May 2019. Intel \u00ae 64 and IA-32 Architectures Software Developer\u2019s Manual Combined Volumes: 1 2A 2B 2C 2D 3A 3B 3C 3D and 4. Online. Order Number: 325462-070US. https:\/\/software.intel.com\/en-us\/articles\/intel-sdm .  Intel Corporation. May 2019. Intel \u00ae 64 and IA-32 Architectures Software Developer\u2019s Manual Combined Volumes: 1 2A 2B 2C 2D 3A 3B 3C 3D and 4. Online. Order Number: 325462-070US. https:\/\/software.intel.com\/en-us\/articles\/intel-sdm ."},{"key":"e_1_3_2_1_21_1","first-page":"319433","article-title":"Intel \u00ae Architecture Instruction Set Extensions Programming Reference","author":"Intel Corporation","year":"2019","unstructured":"Intel Corporation . May , 2019 . Intel \u00ae Architecture Instruction Set Extensions Programming Reference . Order Number : 319433 - 319037 . https:\/\/software.intel.com\/en-us\/articles\/intel-sdm . Intel Corporation. May, 2019. Intel \u00ae Architecture Instruction Set Extensions Programming Reference. Order Number: 319433-037. https:\/\/software.intel.com\/en-us\/articles\/intel-sdm .","journal-title":"Order Number"},{"volume-title":"Symbolic simulation methods for industrial formal verification","author":"Jones Robert B.","key":"e_1_3_2_1_22_1","unstructured":"Robert B. Jones . 2002. Symbolic simulation methods for industrial formal verification . Springer Science & amp; Business Media. Robert B. Jones. 2002. Symbolic simulation methods for industrial formal verification. Springer Science & Business Media."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_19"},{"volume-title":"Replacing Testing with Formal Verification in Intel \u00ae Core TM i7 Processor Execution Engine Validation","author":"Kaivola Roope","key":"e_1_3_2_1_24_1","unstructured":"Roope Kaivola , Rajnish Ghughal , Naren Narasimhan , Amber Telfer , Jesse Whittemore , Sudhindra Pandav , Anna Slobodova , Christopher Taylor , Vladimir Frolov , Erik Reeber , and Armaghan Naik . 2009. Replacing Testing with Formal Verification in Intel \u00ae Core TM i7 Processor Execution Engine Validation . In Computer Aided Verification, Ahmed Bouajjani and Oded Maler (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 414\u2013429. Roope Kaivola, Rajnish Ghughal, Naren Narasimhan, Amber Telfer, Jesse Whittemore, Sudhindra Pandav, Anna Slobodova, Christopher Taylor, Vladimir Frolov, Erik Reeber, and Armaghan Naik. 2009. Replacing Testing with Formal Verification in Intel \u00ae Core TM i7 Processor Execution Engine Validation. In Computer Aided Verification, Ahmed Bouajjani and Oded Maler (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 414\u2013429."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_3"},{"key":"e_1_3_2_1_27_1","unstructured":"Robert S. Boyer and J S. Moore. 1996. Mechanized Formal Reasoning About Programs And Computing Machines. Automated Reasoning and Its Applications: Essays in Honor of Larry Wos (1996) 147\u2013176. https:\/\/www.cs.utexas.edu\/users\/boyer\/bm96.pdf  Robert S. Boyer and J S. Moore. 1996. Mechanized Formal Reasoning About Programs And Computing Machines. Automated Reasoning and Its Applications: Essays in Honor of Larry Wos (1996) 147\u2013176. https:\/\/www.cs.utexas.edu\/users\/boyer\/bm96.pdf"},{"volume-title":"Formal Verification of Floating-Point Hardware Design: A Mathematical Approach","author":"Russinoff David M.","key":"e_1_3_2_1_28_1","unstructured":"David M. Russinoff . 2019. Formal Verification of Floating-Point Hardware Design: A Mathematical Approach . Springer . David M. Russinoff. 2019. Formal Verification of Floating-Point Hardware Design: A Mathematical Approach. Springer."},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2004)","volume":"3312","author":"Ray Sandip","unstructured":"Sandip Ray and J S. Moore . 2004. Proof Styles in Operational Semantics . In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2004) (LNCS), A. J. Hu and A. K. Martin (Eds.) , Vol. 3312 . Springer-Verlag, Austin, TX, 67\u201381. Sandip Ray and J S. Moore. 2004. Proof Styles in Operational Semantics. In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2004) (LNCS), A. J. Hu and A. K. Martin (Eds.), Vol. 3312. Springer-Verlag, Austin, TX, 67\u201381."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9098-1"},{"key":"e_1_3_2_1_32_1","unstructured":"Shilpi Goel and Rob Sumners. 2019. Using x86isa for Microcode Verification. In SpISA 2019: Workshop on Instruction Set Architecture Specification. https:\/\/www.cl.cam.ac.uk\/~jrh13\/spisa19\/paper_08.pdf  Shilpi Goel and Rob Sumners. 2019. Using x86isa for Microcode Verification. In SpISA 2019: Workshop on Instruction Set Architecture Specification. https:\/\/www.cl.cam.ac.uk\/~jrh13\/spisa19\/paper_08.pdf"},{"volume-title":"SAT \u201915: Proceedings of Theory And Applications Of Satisfiability Testing","author":"Slobodova Anna","key":"e_1_3_2_1_33_1","unstructured":"Anna Slobodova . 2015. Pragmatic Approach to Formal Verification . In SAT \u201915: Proceedings of Theory And Applications Of Satisfiability Testing . Springer , LNCS 9340, IX\u2013XI. Anna Slobodova. 2015. Pragmatic Approach to Formal Verification. In SAT \u201915: Proceedings of Theory And Applications Of Satisfiability Testing. Springer, LNCS 9340, IX\u2013XI."},{"key":"e_1_3_2_1_34_1","volume-title":"International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS).","author":"Stewart Daryl","year":"2014","unstructured":"Daryl Stewart , David Gilday , Daniel Nevill , and Thomas Roberts . 2014 . Processor memory system verification using DOGReL: a language for specifying end-to-end properties . In International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS). Daryl Stewart, David Gilday, Daniel Nevill, and Thomas Roberts. 2014. Processor memory system verification using DOGReL: a language for specifying end-to-end properties. In International Workshop on Design and Implementation of Formal Tools and Systems (DIFTS)."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.249.7"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.70.7"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2015.0399"}],"event":{"name":"POPL '20: 47th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"New Orleans LA USA","acronym":"POPL '20"},"container-title":["Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373811","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372885.3373811","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:09Z","timestamp":1750200069000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373811"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,20]]},"references-count":36,"alternative-id":["10.1145\/3372885.3373811","10.1145\/3372885"],"URL":"https:\/\/doi.org\/10.1145\/3372885.3373811","relation":{},"subject":[],"published":{"date-parts":[[2020,1,20]]},"assertion":[{"value":"2020-01-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}