{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:01:50Z","timestamp":1760061710324},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2013,5,23]],"date-time":"2013-05-23T00:00:00Z","timestamp":1369267200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2013,6]]},"DOI":"10.1007\/s11334-013-0195-x","type":"journal-article","created":{"date-parts":[[2013,5,22]],"date-time":"2013-05-22T05:23:03Z","timestamp":1369200183000},"page":"59-77","source":"Crossref","is-referenced-by-count":11,"title":["On construction of a library of formally verified low-level arithmetic functions"],"prefix":"10.1007","volume":"9","author":[{"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,5,23]]},"reference":[{"key":"195_CR1","unstructured":"Affeldt, R., Marti, N.: An Approach to Formal Verification of Arithmetic Functions in Assembly. In: Proceedings of the 11th Annual Asian Computing Science Conference. LNCS, vol. 4435, pp. 346\u2013360. Springer, Heidelberg (2008)."},{"issue":"10\u201311","key":"195_CR2","doi-asserted-by":"crossref","first-page":"1058","DOI":"10.1016\/j.scico.2011.07.003","volume":"77","author":"R Affeldt","year":"2012","unstructured":"Affeldt R, Nowak D, Yamada K (2012) Certifying Assembly with Formal Security Proofs: the Case of BBS. Sci. Comput. Program 77(10\u201311):1058\u20131074","journal-title":"Sci. Comput. Program"},{"key":"195_CR3","unstructured":"Affeldt, R.: On Construction of a Library of Formally Verified Low-level Arithmetic Functions. In: Proceedings of the 27th ACM SIGAPP Symposium On Applied Computing (SAC 2012), Software Verification and Testing Track, vol. 2, pp. 1326\u20131331. ACM (2012)."},{"key":"195_CR4","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Marti, N.: Towards Formal Verification of TLS Network Packet Processing Written in C. In: Proceedings of the 7th ACM SIGPLAN Workshop on Programming Languages meets Program Verification (PLPV 2013), pp. 35\u201346. ACM (2013).","DOI":"10.1145\/2428116.2428124"},{"key":"195_CR5","unstructured":"Affeldt, R.: A Library for Formal Verification of Low-level Programs. Coq documentation. http:\/\/staff.aist.go.jp\/reynald.affeldt\/coqdev (last access: 2013\/02\/25)"},{"key":"195_CR6","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), pp. 14\u201325. ACM (2004).","DOI":"10.1145\/964001.964003"},{"key":"195_CR7","unstructured":"Berghofer, S.: Verification of Dependable Software using Spark and Isabelle. In: Proceedings of the 6th International Workshop on Systems Software Verification Proceedings, pp. 48\u201365 (2011)."},{"key":"195_CR8","doi-asserted-by":"crossref","unstructured":"Boldo, S., Melquiond, G.: Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. In: Proceedings of the 20th IEEE Symposium on Computer Arithmetic (ARITH 2011), pp. 243\u2013252. IEEE Computer Society (2011).","DOI":"10.1109\/ARITH.2011.40"},{"key":"195_CR9","unstructured":"Brent, R.P., Zimmermann, P.: Modern Computer Arithmetic. Version 0.5.9 (7 October 2010). Available at http:\/\/www.loria.fr\/~zimmerma\/mca\/mca-cup-0.5.9.pdf (last access: 2012\/12\/03). Final version published by Cambridge University Press (2010)"},{"key":"195_CR10","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure Microkernels, State Monads and Scalable Refinement. In: Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008). LNCS, vol. 5170, pp. 167\u2013182. Springer, Heidelberg (2008)."},{"key":"195_CR11","unstructured":"Crespo, J.M., Kunz, C.: A Machine-Checked Framework for Relational Separation Logic. In: Proceedings of the 9th International Conference on Software Engineering and Formal Methods (SEFM 2011). LNCS, vol. 7041, pp. 122\u2013137. Springer, Heidelberg (2011)."},{"issue":"4","key":"195_CR12","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1109\/TIT.1985.1057074","volume":"31","author":"T ElGamal","year":"1985","unstructured":"ElGamal T (1985) A public key cryptosystem and a signature scheme based on discrete logarithms. IEEE Transactions on Information Theory 31(4):469\u2013472","journal-title":"IEEE Transactions on Information Theory"},{"key":"195_CR13","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq System. Technical Report 6455. Version 11. INRIA (2012)."},{"key":"195_CR14","doi-asserted-by":"crossref","unstructured":"Hur, C.-K., Dreyer, D.: A Kripke logical relation between ML and assembly. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 133\u2013146. ACM (2011).","DOI":"10.1145\/1926385.1926402"},{"key":"195_CR15","unstructured":"Knuth, D.E.: The Art of Computer Programming. Vol. 2, 3rd edition. Addison-Wesley (1997)."},{"issue":"4","key":"195_CR16","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy X (2009) A formally verified compiler back-end. J. Autom. Reasoning. 43(4):363\u2013446","journal-title":"J. Autom. Reasoning."},{"issue":"2","key":"195_CR17","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"NA Lynch","year":"1995","unstructured":"Lynch NA, Vaandrager FW (1995) Forward and Backward Simulations Part I: Untimed Systems. Inform. Comput. 121(2):214\u2013233","journal-title":"Inform. Comput."},{"key":"195_CR18","unstructured":"Marti, N., Affeldt, R., Yonezawa, A.: Formal Verification of the Heap Manager of an Operating System using Separation Logic. In: Proceedings of the 8th International Conference on Formal Engineering Methods (ICFEM 2006). LNCS, vol. 4260, pp. 400\u2013419. Springer, Heidelberg (2006)."},{"issue":"3","key":"195_CR19","first-page":"135","volume":"25","author":"N Marti","year":"2008","unstructured":"Marti N, Affeldt R (2008) A Certified Verifier for a Fragment of Separation Logic. Computer Software 25(3):135\u2013147","journal-title":"Computer Software"},{"key":"195_CR20","unstructured":"Menezes, A.J., van Oorschot, P.C., Vanstone, S.A.: Handbook of Applied Cryptography. 5th printing. CRC Press (2001)."},{"key":"195_CR21","unstructured":"MIPS Technologies: MIPS32 4KS Processor Core Family Software User\u2019s Manual (2001)."},{"key":"195_CR22","unstructured":"Myreen, M.O., Gordon, M.J.C.: Hoare Logic for Realistically Modelled Machine Code. In: Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007). LNCS, vol. 4424, pp. 568\u2013582. Springer, Heidelberg (2007)."},{"key":"195_CR23","unstructured":"Myreen, M., Gordon, M.: Verification of Machine Code Implementations of Arithmetic Functions for Cryptography. In: TPHOLs Emerging Trends Proceedings. Technical report 364\/07. Department of Computer Science, University of Kaiserslautern (2007)."},{"key":"195_CR24","doi-asserted-by":"crossref","unstructured":"Myreen, M.O.: Verified just-in-time compiler on x86. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2010), pp. 107\u2013118. ACM (2010).","DOI":"10.1145\/1706299.1706313"},{"key":"195_CR25","unstructured":"Reynolds, J.C.: The Craft of Programming. Prentice-Hall, International (1981)."},{"key":"195_CR26","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55\u201374. IEEE Computer Society (2002).","DOI":"10.1109\/LICS.2002.1029817"},{"key":"195_CR27","unstructured":"Shoup, V.: NTL: A Library for doing Number Theory. Version 5.5.2. Available at http:\/\/www.shoup.net\/ntl (last access: 2012\/12\/03) (2009)"},{"key":"195_CR28","unstructured":"Tan, G., Appel, A.W.: A Compositional Logic for Control Flow. In: Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2006). LNCS, vol. 3855, pp. 80\u201394. Springer, Heidelberg (2006)."},{"key":"195_CR29","unstructured":"The Coq Proof Assistant: Reference Manual. Ver. 8.4. Available at http:\/\/coq.inria.fr . INRIA (2012)"},{"key":"195_CR30","unstructured":"The Coq Proof Assistant: Frequently Asked Questions. Available at http:\/\/coq.inria.fr\/faq . INRIA (2012)"},{"key":"195_CR31","unstructured":"The GNU Multi Precision Arithmetic Library. Edition 5.0.2. http:\/\/gmplib.org\/ (2011)"},{"key":"195_CR32","unstructured":"Winwood, S., Klein, G., Sewell, T., Andronick, J., Cock, D., Norrish, M.: Mind the Gap: A Verification Framework for Low-level C. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009). LNCS, vol. 5674, pp. 500\u2013515. Springer, Heidelberg (2009)."},{"issue":"1\u20133","key":"195_CR33","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1016\/j.tcs.2006.12.036","volume":"375","author":"H Yang","year":"2007","unstructured":"Yang H (2007) Relational separation logic. Theor. Comput. Sci. 375(1\u20133):308\u2013334","journal-title":"Theor. Comput. Sci."}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-013-0195-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11334-013-0195-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-013-0195-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,14]],"date-time":"2019-07-14T01:16:18Z","timestamp":1563066978000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11334-013-0195-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5,23]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,6]]}},"alternative-id":["195"],"URL":"https:\/\/doi.org\/10.1007\/s11334-013-0195-x","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,5,23]]}}}