{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:52:58Z","timestamp":1743072778790,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031223075"},{"type":"electronic","value":"9783031223082"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-22308-2_17","type":"book-chapter","created":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T19:55:03Z","timestamp":1669924503000},"page":"372-396","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Semantic Foundations for\u00a0Cost Analysis of\u00a0Pipeline-Optimized Programs"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adrien","family":"Koutsos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sol\u00e8ne","family":"Mirliaz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Schwabe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,12,2]]},"reference":[{"key":"17_CR1","unstructured":"Companion report. https:\/\/hal.inria.fr\/hal-03779257"},{"key":"17_CR2","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9174-1","volume":"46","author":"E Albert","year":"2011","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reason. 46, 161\u2013203 (2011)","journal-title":"J. Autom. Reason."},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., et al.: Jasmin: high-assurance and high-speed cryptography. In: Proceedings of CCS\u20192017, pp. 1807\u20131823. ACM (2017)","DOI":"10.1145\/3133956.3134078"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., et al.: The last mile: high-assurance and high-speed cryptographic implementations. In: Proceedings of S &P\u20192020, pp. 965\u2013982. IEEE (2020)","DOI":"10.1109\/SP40000.2020.00028"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Barbosa, M., et al.: SoK: computer-aided cryptography. In: Proceedings of S &P 2021, pp. 777\u2013795. IEEE (2021)","DOI":"10.1109\/SP40001.2021.00008"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10082-1_6"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/11502760_3","volume-title":"Fast Software Encryption","author":"DJ Bernstein","year":"2005","unstructured":"Bernstein, D.J.: The Poly1305-AES message-authentication code. In: Gilbert, H., Handschuh, H. (eds.) FSE 2005. LNCS, vol. 3557, pp. 32\u201349. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11502760_3"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/11745853_14","volume-title":"Public Key Cryptography - PKC 2006","author":"DJ Bernstein","year":"2006","unstructured":"Bernstein, D.J.: Curve25519: new Diffie-Hellman speed records. In: Yung, M., Dodis, Y., Kiayias, A., Malkin, T. (eds.) PKC 2006. LNCS, vol. 3958, pp. 207\u2013228. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11745853_14"},{"key":"17_CR9","unstructured":"Bernstein, D.J.: ChaCha, a variant of Salsa20. In: Workshop Record of SASC 2008: The State of the Art of Stream Ciphers (2008)"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Cauligi, S., et al.: Constant-time foundations for the new spectre era. In: Proceedings of PLDI\u20192020, pp. 913\u2013926. ACM (2020)","DOI":"10.1145\/3385412.3385970"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"\u00c7i\u00e7ek, E., Barthe, G., Gaboardi, M., Garg, D., Hoffmann, J.: Relational cost analysis. In: Proceedings of POPL 2017, pp. 316\u2013329. ACM (2017)","DOI":"10.1145\/3093333.3009858"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P Cousot","year":"2005","unstructured":"Cousot, P., et al.: The ASTRE\u00c9 analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21\u201330. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_3"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Crary, K., Weirich, S.: Resource bound certification. In: Proceedings of POPL 2000, pp. 184\u2013198. ACM (2000)","DOI":"10.1145\/325694.325716"},{"key":"17_CR15","unstructured":"Daemen, J., Rijmen, V.: AES proposal: Rijndael, version 2 (1999). http:\/\/csrc.nist.gov\/archive\/aes\/rijndael\/Rijndael-ammended.pdf"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/3-540-45449-7_32","volume-title":"Embedded Software","author":"C Ferdinand","year":"2001","unstructured":"Ferdinand, C., et al.: Reliable and precise WCET determination for a real-life processor. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 469\u2013485. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45449-7_32"},{"key":"17_CR17","unstructured":"Fog, A.: The microarchitecture of Intel, AMD and VIA CPUs - An optimization guide for assembly programmers and compiler makers (2020). https:\/\/www.agner.org\/optimize\/microarchitecture.pdf"},{"key":"17_CR18","unstructured":"Fog, A.: The microarchitecture of Intel, AMD and VIA CPUs - instruction tables (2020). https:\/\/www.agner.org\/optimize\/instruction_tables.pdf"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.M.: SPEED: precise and efficient static estimation of program computational complexity. In: Proceedings of POPL 2009, pp. 127\u2013139. ACM (2009)","DOI":"10.1145\/1594834.1480898"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Hahn, S., Reineke, J.: Design and analysis of SIC: a provably timing-predictable pipelined processor core. In: Proceedings of RTSS 2018, pp. 469\u2013481. IEEE (2018)","DOI":"10.1109\/RTSS.2018.00060"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Hughes, J., Pareto, L.: Recursion and dynamic data-structures in bounded space: towards embedded ML programming. In: Proceedings of ICFP 1999. pp. 70\u201381. ACM (1999)","DOI":"10.1145\/317765.317785"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Knoth, T., Wang, D., Polikarpova, N., Hoffmann, J.: Resource-guided program synthesis. In: Proceedings of PLDI 2019, pp. 253\u2013268. ACM (2019)","DOI":"10.1145\/3314221.3314602"},{"key":"17_CR23","doi-asserted-by":"crossref","unstructured":"Knoth, T., Wang, D., Reynolds, A., Hoffmann, J., Polikarpova, N.: Liquid resource types. In: Proceedings of ICFP 2020, pp. 106:1\u2013106:29 (2020)","DOI":"10.1145\/3408988"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Ngo, V.C., Dehesa-Azuara, M., Fredrikson, M., Hoffmann, J.: Verifying and synthesizing constant-resource implementations with types. In: Proceedings of SP 2017, pp. 710\u2013728. IEEE Computer Society (2017)","DOI":"10.1109\/SP.2017.53"},{"issue":"2","key":"17_CR25","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1016\/0167-6423(87)90029-3","volume":"9","author":"HR Nielson","year":"1987","unstructured":"Nielson, H.R.: A Hoare-like proof system for analysing the computation time of programs. Sci. Comput. Program. 9(2), 107\u2013136 (1987)","journal-title":"Sci. Comput. Program."},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"Reistad, B., Gifford, D.K.: Static dependent costs for estimating execution time. In: Proceedings of LFP1994, pp. 65\u201378. ACM (1994)","DOI":"10.1145\/182590.182439"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Reparaz, O., Balasch, J., Verbauwhede, I.: Dude, is my code constant time? In: Proceedings of DATE 2017, pp. 1697\u20131702. IEEE (2017)","DOI":"10.23919\/DATE.2017.7927267"},{"issue":"4","key":"17_CR28","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1145\/321978.321987","volume":"23","author":"B Wegbreit","year":"1976","unstructured":"Wegbreit, B.: Verifying program performance. J. ACM 23(4), 691\u2013699 (1976)","journal-title":"J. ACM"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Wilhelm, R., Grund, D., Reineke, J., Schlickling, M., Pister, M., Ferdinand, C.: Memory hierarchies, pipelines, and buses for future architectures in time-critical embedded systems. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 28(7), 966\u2013978 (2009)","DOI":"10.1109\/TCAD.2009.2013287"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Yourst, M.T.: PTLsim: a cycle accurate full system x86-64 microarchitectural simulator. In: Proceedings of ISPASS 2019, pp. 23\u201334. IEEE Computer Society (2007)","DOI":"10.1109\/ISPASS.2007.363733"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22308-2_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T19:57:08Z","timestamp":1669924628000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22308-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223075","9783031223082"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22308-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"2 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Auckland","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"New Zealand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 December 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 December 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.staticanalysis.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"18","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"42% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6.1","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}