{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,27]],"date-time":"2025-01-27T05:17:48Z","timestamp":1737955068105,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540775041"},{"type":"electronic","value":"9783540775058"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-77505-8_27","type":"book-chapter","created":{"date-parts":[[2008,1,24]],"date-time":"2008-01-24T12:56:35Z","timestamp":1201179395000},"page":"346-360","source":"Crossref","is-referenced-by-count":5,"title":["An Approach to Formal Verification of Arithmetic Functions in Assembly"],"prefix":"10.1007","author":[{"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[]},{"given":"Nicolas","family":"Marti","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"10","key":"27_CR1","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM\u00a012(10), 576\u2013585 (1969)","journal-title":"Communications of the ACM"},{"issue":"170","key":"27_CR2","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1090\/S0025-5718-1985-0777282-X","volume":"44","author":"P.L. Montgomery","year":"1985","unstructured":"Montgomery, P.L.: Modular multiplication without trial division. Mathematics of Computation\u00a044(170), 519\u2013521 (1985)","journal-title":"Mathematics of Computation"},{"key":"27_CR3","unstructured":"Various contributors. The Coq Proof assistant. http:\/\/coq.inria.fr"},{"issue":"3","key":"27_CR4","first-page":"23","volume":"16","author":"C.K. Koc","year":"1996","unstructured":"Koc, C.K., Acar, T., Kaliski Jr, B.S.: Analyzing and Comparing Montgomery Multiplication Algorithms. IEEE Micro\u00a016(3), 23\u201326 (1996)","journal-title":"IEEE Micro"},{"key":"27_CR5","unstructured":"MIPS Technologies. MIPS32 4KS Processor Core Family Software User\u2019s Manual MIPS Technologies, Inc., 1225 Charleston Road, Mountain View, CA 94043-1353"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS 2002. 17th IEEE Symposium on Logic in Computer Science, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Hamid, N.A., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A Syntactic Approach to Foundational Proof-Carrying Code. In: LICS 2002. 7th IEEE Symposium on Logic In Computer Science, pp. 89\u2013100 (2002)","DOI":"10.1109\/LICS.2002.1029819"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-36575-3_25","volume-title":"Programming Languages and Systems","author":"D. Yu","year":"2003","unstructured":"Yu, D., Hamid, N.A., Shao, Z.: Building Certified Libraries for PCC: Dynamic Storage Allocation. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol.\u00a02618, pp. 363\u2013379. Springer, Heidelberg (2003)"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-30142-4_10","volume-title":"Theorem Proving in Higher Order Logics","author":"N.A. Hamid","year":"2004","unstructured":"Hamid, N.A., Shao, Z.: Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 118\u2013135. Springer, Heidelberg (2004)"},{"key":"27_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30124-0_21","volume-title":"Computer Science Logic","author":"T. Weber","year":"2004","unstructured":"Weber, T.: Towards Mechanized Program Verification with Separation Logic. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, Springer, Heidelberg (2004)"},{"key":"27_CR11","unstructured":"Babi\u0107, D., Musuvathi, M.: Modular Arithmetic Decision Procedure. Microsoft Research Technical Report. MSR-TR-2005-114"},{"key":"27_CR12","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1016\/j.entcs.2005.09.031","volume":"156","author":"A. Saabas","year":"2006","unstructured":"Saabas, A., Uustalu, T.: A Compositional Natural Semantics and Hoare Logic for Low-Level Languages. Electronic Notes in Theoretical Computer Science\u00a0156, 151\u2013168 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/11609773_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G. Tan","year":"2005","unstructured":"Tan, G., Appel, A.W.: A Compositional Logic for Control Flow. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 80\u201394. Springer, Heidelberg (2005)"},{"key":"27_CR14","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: POPL 2006. 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 42\u201365","DOI":"10.1145\/1111037.1111042"},{"key":"27_CR15","doi-asserted-by":"crossref","unstructured":"Chlipala, A.J.: Modular development of certified program verifiers with a proof assistant. In: ICFP 2006. 11th ACM SIGPLAN International Conference on Functional Programming, pp. 160\u2013171 (2006)","DOI":"10.1145\/1159803.1159825"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/11901433_22","volume-title":"Formal Methods and Software Engineering","author":"N. Marti","year":"2006","unstructured":"Marti, N., Affeldt, R., Yonezawa, A.: Formal Verification of the Heap Manager of an Operating System using Separation Logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 400\u2013419. Springer, Heidelberg (2006)"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Marti, N.: An Approach to Formal Verification of Arithmetic Functions in Assembly|Proof Scripts, http:\/\/staff.aist.go.jp\/reynald.affeldt\/seplog\/asian2006","DOI":"10.1007\/978-3-540-77505-8_27"}],"container-title":["Lecture Notes in Computer Science","Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-77505-8_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,26]],"date-time":"2025-01-26T06:39:10Z","timestamp":1737873550000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-77505-8_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540775041","9783540775058"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-77505-8_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}