{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T10:10:02Z","timestamp":1746267002555,"version":"3.40.4"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319076010"},{"type":"electronic","value":"9783319076027"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[[2014]]},"DOI":"10.1007\/978-3-319-07602-7_4","type":"book-chapter","created":{"date-parts":[[2014,6,12]],"date-time":"2014-06-12T11:29:08Z","timestamp":1402572548000},"page":"23-40","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Proof-Carrying Code Approach to Certificate Auction Mechanisms"],"prefix":"10.1007","author":[{"given":"W.","family":"Bai","sequence":"first","affiliation":[]},{"given":"E. M.","family":"Tadjouddine","sequence":"additional","affiliation":[]},{"given":"T. R.","family":"Payne","sequence":"additional","affiliation":[]},{"given":"S. U.","family":"Guan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,6,13]]},"reference":[{"issue":"5","key":"4_CR1","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1038\/scientificamerican0501-34","volume":"284","author":"T Berners-Lee","year":"2001","unstructured":"Berners-Lee, T., Hendler, J., Lassila, O., et al.: The semantic web. Sci. Am. 284(5), 28\u201337 (2001)","journal-title":"Sci. Am."},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Necula, G.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 106\u2013119. ACM (1997)","DOI":"10.1145\/263699.263712"},{"key":"4_CR3","unstructured":"The Coq Development Team: The coq proof assistant reference manual: Version 8.4 (2012) http:\/\/coq.inria.fr"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-540-75254-7_29","volume-title":"Multi-Agent Systems and Applications V","author":"EM Tadjouddine","year":"2007","unstructured":"Tadjouddine, E.M., Guerin, F.: Verifying dominant strategy equilibria in auctions. In: Burkhard, H.-D., Lindemann, G., Verbrugge, R., Varga, L.Z. (eds.) CEEMAS 2007. LNCS (LNAI), vol. 4696, pp. 288\u2013297. Springer, Heidelberg (2007)"},{"key":"4_CR5","unstructured":"Tadjouddine, E., Guerin, F., Vasconcelos, W.: Abstractions for model-checking game-theoretic properties of auctions. In: Proceedings of the 7th International Joint Conference on Autonomous Agents and Multiagent Systems-Volume 3, International Foundation for Autonomous Agents and Multiagent Systems, pp. 1613\u20131616 (2008)"},{"issue":"2","key":"4_CR6","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1108\/17563781111136676","volume":"4","author":"EM Tadjouddine","year":"2011","unstructured":"Tadjouddine, E.M.: Computational complexity of some intelligent computing systems. Int. J. Intell. Comput. Cybernetics 4(2), 144\u2013159 (2011)","journal-title":"Int. J. Intell. Comput. Cybernetics"},{"issue":"3","key":"4_CR7","first-page":"121","volume":"3","author":"F Tip","year":"1995","unstructured":"Tip, F.: A survey of program slicing techniques. J. Program. Lang. 3(3), 121\u2013189 (1995)","journal-title":"J. Program. Lang."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Dolev, S., Panagopoulou, P., Rabie, M., Schiller, E., Spirakis, P.: Rationality authority for provable rational behavior. In: Proceedings of the 30th Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pp. 289\u2013290. ACM (2011)","DOI":"10.1145\/1993806.1993858"},{"key":"4_CR9","unstructured":"Lapets, A., Levin, A., Parkes, D.: A typed language for truthful one-dimensional mechanism design. Technical report, Computer Science Department, Boston University (2008)"},{"issue":"2","key":"4_CR10","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.entcs.2005.02.043","volume":"141","author":"A S\u0103lcianu","year":"2005","unstructured":"S\u0103lcianu, A., Arkoudas, K.: Machine-checkable correctness proofs for intra-procedural dataflow analyses. Electr. Notes Theoret. Comput. Sci. 141(2), 53\u201368 (2005)","journal-title":"Electr. Notes Theoret. Comput. Sci."},{"key":"4_CR11","unstructured":"Dowek, G., Felty, A., Herbelin, H., Huet, G., Werner, B., Paulin-Mohring, C., et al.: The coq proof assistant user\u2019s guide: Version 5.6 (1991)"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-36532-X_14","volume-title":"Software Security \u2013 Theories and Systems","author":"R Affeldt","year":"2003","unstructured":"Affeldt, R., Kobayashi, N.: Formalization and Verification of a Mail Server in Coq. In: Okada, M., Pierce, B., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol. 2609, pp. 217\u2013233. Springer, Heidelberg (2003)"},{"issue":"7","key":"4_CR13","doi-asserted-by":"publisher","first-page":"117","DOI":"10.2197\/ipsjdc.1.117","volume":"1","author":"R Affeldt","year":"2005","unstructured":"Affeldt, R., Kobayashi, N., Yonezawa, A.: Verification of concurrent programs using the coq proof assistant: a case study. IPSJ Digital Courier 1(7), 117\u2013127 (2005)","journal-title":"IPSJ Digital Courier"},{"issue":"7","key":"4_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-87827-8_28","volume-title":"Computer Mathematics","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, p. 333. Springer, Heidelberg (2008)"},{"issue":"2","key":"4_CR16","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1016\/j.ipl.2005.09.010","volume":"97","author":"R Vestergaard","year":"2006","unstructured":"Vestergaard, R.: A constructive approach to sequential nash equilibria. Inf. Process. Lett. 97(2), 46\u201351 (2006)","journal-title":"Inf. Process. Lett."},{"key":"4_CR17","series-title":"International Federation for Information Processing","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-1-4020-8157-6_27","volume-title":"Building the Information Society","author":"P Cousot","year":"2004","unstructured":"Cousot, P., Cousot, R.: Basic concepts of abstract interpretation. In: Jacquart, R. (ed.) Building the Information Society. IFIP, vol. 156, pp. 359\u2013366. Springer, Heidelberg (2004)"},{"issue":"1","key":"4_CR18","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1145\/565816.503290","volume":"37","author":"P Cousot","year":"2002","unstructured":"Cousot, P., Cousot, R.: Systematic design of program transformation frameworks by abstract interpretation. ACM SIGPLAN Not. 37(1), 178\u2013190 (2002)","journal-title":"ACM SIGPLAN Not."},{"key":"4_CR19","volume-title":"Handbook of Logic in Computer Science","author":"H Barendregt","year":"1992","unstructured":"Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. ii. Oxford University Press, Oxford (1992)"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Appel, A.: Foundational proof-carrying code. In: 16th Annual IEEE Symposium on Logic in Computer Science, Proceedings, pp. 247\u2013256. IEEE (2001)","DOI":"10.1109\/LICS.2001.932501"},{"key":"4_CR21","volume-title":"Game Theory","author":"D Fudenberg","year":"1991","unstructured":"Fudenberg, D., Tirole, J.: Game Theory. MIT Press, Cambridge (1991)"},{"key":"4_CR22","doi-asserted-by":"publisher","DOI":"10.1002\/9780470058411","volume-title":"Developing Multi-agent Systems with JADE (wiley series in agent technology)","author":"F Bellifemine","year":"2007","unstructured":"Bellifemine, F., Caire, G., Greenwood, D.: Developing Multi-agent Systems with JADE (wiley series in agent technology). Wiley, Chichester (2007)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Component Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-07602-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T09:44:04Z","timestamp":1746265444000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-07602-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319076010","9783319076027"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-07602-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"13 June 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}