{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:00:39Z","timestamp":1760061639969},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319723075"},{"type":"electronic","value":"9783319723082"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-72308-2_5","type":"book-chapter","created":{"date-parts":[[2017,12,14]],"date-time":"2017-12-14T13:25:15Z","timestamp":1513257915000},"page":"66-83","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Verifying Branch-Free Assembly Code in Why3"],"prefix":"10.1007","author":[{"given":"Marc","family":"Schoolderman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,15]]},"reference":[{"unstructured":"Atmel Corporation: AVR Instruction Set Manual, revision 0856L (2016)","key":"5_CR1"},{"doi-asserted-by":"crossref","unstructured":"Barthe, G., Betarte, G., Campo, J., Luna, C., Pichardie, D.: System-level non-interference for constant-time cryptography. In: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS 2014, pp. 1267\u20131279. ACM, New York (2014)","key":"5_CR2","DOI":"10.1145\/2660267.2660283"},{"unstructured":"Bernstein, D.J.: qhasm: tools to help write high-speed software. \nhttp:\/\/cr.yp.to\/qhasm.html\n\n. Accessed 01 Dec 2016","key":"5_CR3"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-27954-6_11","volume-title":"Topics in Cryptology \u2013 CT-RSA 2012","author":"BB Brumley","year":"2012","unstructured":"Brumley, B.B., Barbosa, M., Page, D., Vercauteren, F.: Practical realisation and elimination of an ECC-related software bug attack. In: Dunkelman, O. (ed.) CT-RSA 2012. LNCS, vol. 7178, pp. 171\u2013186. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-27954-6_11"},{"doi-asserted-by":"crossref","unstructured":"Chen, Y.F., Hsu, C.H., Lin, H.H., Schwabe, P., Tsai, M.H., Wang, B.Y., Yang, B.Y., Yang, S.Y.: Verifying Curve25519 software. In: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS 2014, pp. 299\u2013309. ACM (2014)","key":"5_CR5","DOI":"10.1145\/2660267.2660370"},{"issue":"2\u20133","key":"5_CR6","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/s10623-015-0087-1","volume":"77","author":"M D\u00fcll","year":"2015","unstructured":"D\u00fcll, M., Haase, B., Hinterw\u00e4lder, G., Hutter, M., Paar, C., S\u00e1nchez, A.H., Schwabe, P.: High-speed Curve25519 on 8-bit, 16-bit, and 32-bit microcontrollers. Des. Codes Crypt. 77(2\u20133), 493\u2013514 (2015)","journal-title":"Des. Codes Crypt."},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-08867-9_1","volume-title":"Computer Aided Verification","author":"J-C Filli\u00e2tre","year":"2014","unstructured":"Filli\u00e2tre, J.-C., Gondelman, L., Paskevich, A.: The spirit of ghost code. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 1\u201316. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08867-9_1"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 Where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"issue":"3","key":"5_CR9","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/s13389-015-0093-2","volume":"5","author":"M Hutter","year":"2015","unstructured":"Hutter, M., Schwabe, P.: Multiprecision multiplication on AVR revisited. J. Cryptographic Eng. 5(3), 201\u2013214 (2015)","journal-title":"J. Cryptographic Eng."},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-41010-9_11","volume-title":"Formal Methods for Industrial Critical Systems","author":"P Jackson","year":"2013","unstructured":"Jackson, P., Schanda, F., Wallenburg, A.: Auditing user-provided axioms in software verification conditions. In: Pecheur, C., Dierkes, M. (eds.) FMICS 2013. LNCS, vol. 8187, pp. 154\u2013168. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-41010-9_11"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1007\/3-540-48405-1_25","volume-title":"Advances in Cryptology \u2014 CRYPTO 1999","author":"P Kocher","year":"1999","unstructured":"Kocher, P., Jaffe, J., Jun, B.: Differential power analysis. In: Wiener, M. (ed.) CRYPTO 1999. LNCS, vol. 1666, pp. 388\u2013397. Springer, Heidelberg (1999). \nhttps:\/\/doi.org\/10.1007\/3-540-48405-1_25"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-319-21966-0_12","volume-title":"Information and Communications Security","author":"Z Liu","year":"2015","unstructured":"Liu, Z., Seo, H., Gro\u00dfsch\u00e4dl, J., Kim, H.: Reverse product-scanning multiplication and squaring on 8-bit AVR processors. In: Hui, L.C.K., Qing, S.H., Shi, E., Yiu, S.M. (eds.) ICICS 2014. LNCS, vol. 8958, pp. 158\u2013175. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21966-0_12"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11734727_14","volume-title":"Information Security and Cryptology - ICISC 2005","author":"D Molnar","year":"2006","unstructured":"Molnar, D., Piotrowski, M., Schultz, D., Wagner, D.: The program counter security model: automatic detection and removal of control-flow side channel attacks. In: Won, D.H., Kim, S. (eds.) ICISC 2005. LNCS, vol. 3935, pp. 156\u2013168. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11734727_14"},{"doi-asserted-by":"crossref","unstructured":"Pereira, M., de Sousa, S.M.: Complexity checking of ARM programs, by deduction. In: Proceedings of the 29th Annual ACM Symposium on Applied Computing, SAC 2014, pp. 1309\u20131314. ACM, New York (2014)","key":"5_CR14","DOI":"10.1145\/2554850.2555012"},{"unstructured":"Schwabe, P., Schmaltz, J.: Verification of optimised 48-bit multiplications on AVR. Radboud University, Technical report (2015)","key":"5_CR15"},{"unstructured":"Yu, Y.: Automated proofs of object code for a widely used microprocessor. University of Texas at Austin, Austin, TX, USA, Technical report (1993)","key":"5_CR16"}],"container-title":["Lecture Notes in Computer Science","Verified Software. Theories, Tools, and Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-72308-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,12,14]],"date-time":"2017-12-14T13:27:15Z","timestamp":1513258035000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-72308-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319723075","9783319723082"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-72308-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}