{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T05:04:16Z","timestamp":1755839056492,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030636173"},{"type":"electronic","value":"9783030636180"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-63618-0_9","type":"book-chapter","created":{"date-parts":[[2020,12,5]],"date-time":"2020-12-05T08:04:14Z","timestamp":1607155454000},"page":"144-160","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Verification of an Optimized NTT Algorithm"],"prefix":"10.1007","author":[{"given":"Jorge A.","family":"Navas","sequence":"first","affiliation":[]},{"given":"Bruno","family":"Dutertre","sequence":"additional","affiliation":[]},{"given":"Ian A.","family":"Mason","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,12,6]]},"reference":[{"key":"9_CR1","unstructured":"Alkim, E., Ducas, L., P\u00f6ppelmann, T., Schwabe, P.: Post-quantum key exchange - a new hope. In: USENIX Security Symposium, pp. 327\u2013343 (2016)"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-642-38856-9_4","volume-title":"Static Analysis","author":"G Amato","year":"2013","unstructured":"Amato, G., Scozzari, F.: Localizing widening and narrowing. In: Logozzo, F., F\u00e4hndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 25\u201342. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38856-9_4"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Blanchet, B., et al.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T., Schmidt, D., Sudborough, I.H. (eds.) The Essence of Computation: Complexity, Analysis, Transformation (2002)","DOI":"10.1007\/3-540-36377-7_5"},{"key":"9_CR5","unstructured":"Clam: Crab for LLVM Abstraction Manager. https:\/\/github.com\/seahorn\/crab-llvm"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"issue":"90","key":"9_CR7","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1090\/S0025-5718-1965-0178586-1","volume":"19","author":"JW Cooley","year":"1965","unstructured":"Cooley, J.W., Tukey, J.W.: An algorithm for the machine calculation of complex Fourier series. Math. Comput. 19(90), 297\u2013301 (1965)","journal-title":"Math. Comput."},{"key":"9_CR8","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: ISOP 1976, pp. 106\u2013130 (1976)"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: POPL, pp. 105\u2013118. ACM (2011)","DOI":"10.1145\/1925844.1926399"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) POPL 1978, pp. 84\u201396. ACM Press (1978)","DOI":"10.1145\/512760.512770"},{"key":"9_CR12","unstructured":"CoRnucopia of ABstractions: A language-agnostic library for abstract interpretation. https:\/\/github.com\/seahorn\/crab"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33826-7_16"},{"key":"9_CR14","unstructured":"BLISS Implementation: Bimodal Lattice Signature Schemes. https:\/\/github.com\/SRI-CSL\/Bliss"},{"key":"9_CR15","unstructured":"An Implementation of the Number Theoretic Transform. https:\/\/github.com\/SRI-CSL\/NTT"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-11957-6_14","volume-title":"Programming Languages and Systems","author":"I Dillig","year":"2010","unstructured":"Dillig, I., Dillig, T., Aiken, A.: Fluid updates: beyond strong vs. weak updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 246\u2013266. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11957-6_14"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-319-48869-1_5","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"R Dockins","year":"2016","unstructured":"Dockins, R., Foltzer, A., Hendrix, J., Huffman, B., McNamee, D., Tomb, A.: Constructing semantic models of programs with the software analysis workbench. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 56\u201372. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_5"},{"key":"9_CR18","unstructured":"Ducas, L.: Accelerating Bliss: the geometry of ternary polynomials. Cryptology ePrint Archive, Report 2014\/874 (2014). http:\/\/eprint.iacr.org\/2014\/874"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-642-40041-4_3","volume-title":"Advances in Cryptology \u2013 CRYPTO 2013","author":"L Ducas","year":"2013","unstructured":"Ducas, L., Durmus, A., Lepoint, T., Lyubashevsky, V.: Lattice signatures and bimodal Gaussians. In: Canetti, R., Garay, J.A. (eds.) CRYPTO 2013. LNCS, vol. 8042, pp. 40\u201356. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40041-4_3"},{"key":"9_CR20","unstructured":"Fog, A.: Instruction tables: instruction latencies, throughputs and micro-operation breakdowns for Intel, AMD and VIA CPUs (2020). www.agner.org\/optimize"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Gentleman, W.M., Sande, G.: Fast Fourier transforms\u2013for fun and profit. In: AFIPS 1966, pp. 563\u2013578 (1966). https:\/\/doi.org\/10.1145\/1464291.1464352","DOI":"10.1145\/1464291.1464352"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: POPL, pp. 338\u2013350. ACM (2005)","DOI":"10.1145\/1047659.1040333"},{"key":"9_CR23","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1080\/00207168908803778","volume":"30","author":"P Granger","year":"1989","unstructured":"Granger, P.: Static analysis of arithmetical congruences. Int. J. Comput. Math. 30, 165\u2013190 (1989)","journal-title":"Int. J. Comput. Math."},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343\u2013361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. In: PLDI, pp. 339\u2013348. ACM (2008)","DOI":"10.1145\/1379022.1375623"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Harvey, D.: Faster arithmetic for number-theoretic transforms. J. Symb. Comput. 60, 113\u2013119 (2014). https:\/\/doi.org\/10.1016\/j.jsc.2013.09.002","DOI":"10.1016\/j.jsc.2013.09.002"},{"issue":"3","key":"9_CR27","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10703-016-0249-4","volume":"48","author":"A Komuravelli","year":"2016","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), 175\u2013205 (2016). https:\/\/doi.org\/10.1007\/s10703-016-0249-4","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-24372-1_38","volume-title":"Automated Technology for Verification and Analysis","author":"L Lakhdar-Chaouch","year":"2011","unstructured":"Lakhdar-Chaouch, L., Jeannet, B., Girault, A.: Widening with thresholds for programs with complex control graphs. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 492\u2013502. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24372-1_38"},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-319-48965-0_8","volume-title":"Cryptology and Network Security","author":"P Longa","year":"2016","unstructured":"Longa, P., Naehrig, M.: Speeding up the number theoretic transform for faster ideal lattice-based cryptography. In: Foresti, S., Persiano, G. (eds.) CANS 2016. LNCS, vol. 10052, pp. 124\u2013139. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48965-0_8"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-44978-7_10","volume-title":"Programs as Data Objects","author":"A Min\u00e9","year":"2001","unstructured":"Min\u00e9, A.: A new numerical abstract domain based on difference-bound matrices. In: Danvy, O., Filinski, A. (eds.) PADO 2001. LNCS, vol. 2053, pp. 155\u2013172. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44978-7_10"},{"issue":"1","key":"9_CR31","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High.-Order Symb. Comput. 19(1), 31\u2013100 (2006)","journal-title":"High.-Order Symb. Comput."},{"issue":"170","key":"9_CR32","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1090\/S0025-5718-1985-0777282-X","volume":"44","author":"PL Montgomery","year":"1985","unstructured":"Montgomery, P.L.: Modular multiplication without trial division. Math. Comput. 44(170), 519\u2013521 (1985)","journal-title":"Math. Comput."},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-642-33481-8_8","volume-title":"Progress in Cryptology \u2013 LATINCRYPT 2012","author":"T P\u00f6ppelmann","year":"2012","unstructured":"P\u00f6ppelmann, T., G\u00fcneysu, T.: Towards efficient arithmetic for lattice-based cryptography on reconfigurable hardware. In: Hevia, A., Neven, G. (eds.) LATINCRYPT 2012. LNCS, vol. 7533, pp. 139\u2013158. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33481-8_8"},{"key":"9_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-319-22174-8_19","volume-title":"Progress in Cryptology \u2013 LATINCRYPT 2015","author":"T P\u00f6ppelmann","year":"2015","unstructured":"P\u00f6ppelmann, T., Oder, T., G\u00fcneysu, T.: High-performance ideal lattice-based cryptography on 8-bit ATxmega microcontrollers. In: Lauter, K., Rodr\u00edguez-Henr\u00edquez, F. (eds.) LATINCRYPT 2015. LNCS, vol. 9230, pp. 346\u2013365. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22174-8_19"},{"key":"9_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-662-44709-3_21","volume-title":"Cryptographic Hardware and Embedded Systems \u2013 CHES 2014","author":"SS Roy","year":"2014","unstructured":"Roy, S.S., Vercauteren, F., Mentens, N., Chen, D.D., Verbauwhede, I.: Compact ring-LWE cryptoprocessor. In: Batina, L., Robshaw, M. (eds.) CHES 2014. LNCS, vol. 8731, pp. 371\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44709-3_21"},{"key":"9_CR36","unstructured":"SeaHorn verification framework. https:\/\/github.com\/seahorn\/seahorn"},{"key":"9_CR37","volume-title":"Hacker\u2019s Delight","author":"HS Warren","year":"2013","unstructured":"Warren, H.S.: Hacker\u2019s Delight, 2nd edn. Addison-Wesley, Boston (2013)","edition":"2"},{"key":"9_CR38","series-title":"Texts and Monographs in Symbolic Computation","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-6571-3","volume-title":"Polynomial Algorithms in Computer Algebra","author":"F Winkler","year":"1996","unstructured":"Winkler, F.: Polynomial Algorithms in Computer Algebra. Texts and Monographs in Symbolic Computation. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/978-3-7091-6571-3"}],"container-title":["Lecture Notes in Computer Science","Software Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-63618-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T12:27:57Z","timestamp":1619267277000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-63618-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030636173","9783030636180"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-63618-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"6 December 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VSTTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Working Conference on Verified Software: Theories, Tools, and Experiments","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vstte2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/sri-csl.github.io\/VSTTE20\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"7","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":"4","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":"57% - 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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Due to COVID-19 pandemic the conference was held virtually","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}