HTTP/2 200 date: Wed, 04 Feb 2026 00:08:28 GMT content-type: application/json content-length: 1475 access-control-expose-headers: Link access-control-allow-headers: X-Requested-With, Accept, Accept-Encoding, Accept-Charset, Accept-Language, Accept-Ranges, Cache-Control access-control-allow-origin: * vary: Accept-Encoding content-encoding: gzip server: Jetty(9.4.40.v20210413) x-rate-limit: 5 x-rate-limit-interval: 1s x-concurrency-limit: 1 x-api-pool: public permissions-policy: interest-cohort=() {"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T06:57:39Z","timestamp":1767164259783,"version":"build-2238731810"},"reference-count":12,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"6","license":[{"start":{"date-parts":[[2016,11,1]],"date-time":"2016-11-01T00:00:00Z","timestamp":1477958400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Secur. Privacy"],"published-print":{"date-parts":[[2016,11]]},"DOI":"10.1109\/msp.2016.125","type":"journal-article","created":{"date-parts":[[2016,12,14]],"date-time":"2016-12-14T14:45:07Z","timestamp":1481726707000},"page":"26-33","source":"Crossref","is-referenced-by-count":14,"title":["Automated Verification of Real-World Cryptographic Implementations"],"prefix":"10.1109","volume":"14","author":[{"given":"Aaron","family":"Tomb","sequence":"first","affiliation":[]}],"member":"263","reference":[{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04694-0_6"},{"key":"ref3","first-page":"78","article-title":"Decompilation into Logic-Improved","author":"myreen","year":"0","journal-title":"Proc Formal Methods in Computer Aided Design (FMCAD)"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33260-9_4"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/11814948_13"},{"key":"ref5","first-page":"24","article-title":"ABC: An Academic Industrial-Strength Verification Tool","author":"brayton","year":"0","journal-title":"Proc 22nd Int'l Conf Computer Aided Verification (CAV 10)"},{"key":"ref12","first-page":"71","article-title":"Computer-Aided Security Proofs for the Working Cryptographer","author":"barthe","year":"0","journal-title":"Proc 31 st Ann Conf Advances in Cryptology (CRYPTO 11)"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34961-4_17"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660370"},{"key":"ref2","first-page":"73","article-title":"Pragmatic Equivalence and Safety Checking in Cryptol","author":"erk\u00f6k","year":"0","journal-title":"Proceedings of the 3rd workshop on Programming languages meets program verification - PLPV '09"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29613-5_4"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27954-6_11"}],"container-title":["IEEE Security & Privacy"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8013\/7782693\/07782698.pdf?arnumber=7782698","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T11:58:27Z","timestamp":1641988707000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7782698\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11]]},"references-count":12,"aliases":["10.1109\/msp.2017.265093349"],"journal-issue":{"issue":"6"},"URL":"https:\/\/doi.org\/10.1109\/msp.2016.125","relation":{},"ISSN":["1540-7993"],"issn-type":[{"value":"1540-7993","type":"print"}],"subject":[],"published":{"date-parts":[[2016,11]]}}}