{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T09:32:28Z","timestamp":1758706348650},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540939191"},{"type":"electronic","value":"9783540939207"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-540-93920-7_13","type":"book-chapter","created":{"date-parts":[[2008,12,24]],"date-time":"2008-12-24T09:33:38Z","timestamp":1230111218000},"page":"197-214","source":"Crossref","is-referenced-by-count":7,"title":["Abstracting and Verifying Strategy-Proofness for Auction Mechanisms"],"prefix":"10.1007","author":[{"given":"Emmanuel M.","family":"Tadjouddine","sequence":"first","affiliation":[]},{"given":"Frank","family":"Guerin","sequence":"additional","affiliation":[]},{"given":"Wamberto","family":"Vasconcelos","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"Guerin, F., Tadjouddine, E.M.: Realising common knowledge assumptions in agent auctions. In: The IEEE\/WIC\/ACM Int\u2019l Conf. on Intelligent Agent Technology, Hong Kong, China, pp. 579\u2013586 (2006)","DOI":"10.1109\/IAT.2006.106"},{"key":"13_CR2","first-page":"896","volume-title":"AAMAS 2004","author":"R.H. Bordini","year":"2004","unstructured":"Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: State-space Reduction Techniques in Agent Verification. In: AAMAS 2004, pp. 896\u2013903. ACM Press, New York (2004)"},{"key":"13_CR3","unstructured":"Tadjouddine, E.M., Guerin, F., Vasconcelos, W.: Abstractions for model checking game-theoretic properties in auctions. In: AAMAS (accepted, 2008)"},{"key":"13_CR4","unstructured":"Tennenholtz, M.: Some tractable combinatorial auctions. In: AAAI, pp. 98\u2013103 (2000)"},{"key":"13_CR5","volume-title":"The SPIN Model checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model checker: Primer and Reference Manual. Addison, Boston (2004)"},{"key":"13_CR6","first-page":"121","volume":"3","author":"F. Tip","year":"1995","unstructured":"Tip, F.: A Survey of Program Slicing Techniques. Journal of Progr. Lang.\u00a03, 121\u2013189 (1995)","journal-title":"Journal of Progr. Lang."},{"key":"13_CR7","volume-title":"Combinatorial Auctions","author":"P. Cramton","year":"2006","unstructured":"Cramton, P., Shoham, Y., Steinberg, R.: Combinatorial Auctions. MIT Press, Cambridge (2006)"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"Cavallo, R.: Optimal decision-making with minimal waste: strategyproof redistribution of VCG payments. In: AAMAS, pp. 882\u2013889 (2006)","DOI":"10.1145\/1160633.1160790"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Nisan, N., Ronen, A.: Computationally feasible VCG mechanisms. In: ACM Conference on Electronic Commerce, pp. 242\u2013252 (2000)","DOI":"10.1145\/352871.352898"},{"key":"13_CR10","doi-asserted-by":"publisher","first-page":"1131","DOI":"10.1287\/mnsc.44.8.1131","volume":"44","author":"M.H. Rothkopf","year":"1998","unstructured":"Rothkopf, M.H., Pekec, A., Harstad, R.M.: Computationally manageable combinatorial auctions. Management Science\u00a044, 1131\u20131147 (1998)","journal-title":"Management Science"},{"key":"13_CR11","doi-asserted-by":"publisher","first-page":"1013","DOI":"10.1137\/0218069","volume":"18","author":"H.N. Gabow","year":"1989","unstructured":"Gabow, H.N., Tarjan, R.E.: Faster scaling algorithms for network problems. SIAM J. Comput.\u00a018, 1013\u20131036 (1989)","journal-title":"SIAM J. Comput."},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","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":"E.M. 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, vol.\u00a04696, pp. 288\u2013297. Springer, Heidelberg (2007)"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Jackson, D.: Automating first-order relational logic. In: SIGSOFT FSE, pp. 130\u2013139 (2000)","DOI":"10.1145\/355045.355063"},{"key":"13_CR14","volume-title":"Operations Research: An Introduction","author":"H.A. Taha","year":"1997","unstructured":"Taha, H.A.: Operations Research: An Introduction, 6th edn. Prentice-Hall, Englewood Cliffs (1997)","edition":"6"},{"key":"13_CR15","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1145\/242224.242433","volume":"28","author":"P. Cousot","year":"1996","unstructured":"Cousot, P.: Program Analysis: The Abstract Interpretation Perspective. ACM Computing Surveys\u00a028, 165 (1996)","journal-title":"ACM Computing Surveys"},{"key":"13_CR16","first-page":"238","volume-title":"The Fourth Annual ACM SIGPLAN-SIGACT Symposium on POPL","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: The Fourth Annual ACM SIGPLAN-SIGACT Symposium on POPL, Los Angeles, California, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"13_CR17","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/s10009-002-0088-z","volume":"5","author":"C.S. Pasareanu","year":"2003","unstructured":"Pasareanu, C.S., Dwyer, M.B., Visser, W.: Finding feasible abstract counter-examples. Soft. Tools for Tech. Transfer\u00a05, 34\u201348 (2003)","journal-title":"Soft. Tools for Tech. Transfer"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/978-3-540-45099-3_20","volume-title":"Static Analysis","author":"H. Sa\u00efdi","year":"2000","unstructured":"Sa\u00efdi, H.: Model checking guided abstraction and analysis. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 377\u2013396. Springer, Heidelberg (2000)"},{"key":"13_CR19","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10458-006-5955-7","volume":"12","author":"R.H. Bordini","year":"2006","unstructured":"Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying Multi-Agent Programs by Model Checking. Autonomous Agents and Multi-Agent Systems\u00a012, 239\u2013256 (2006)","journal-title":"Autonomous Agents and Multi-Agent Systems"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/BFb0031845","volume-title":"Agents Breaking Away","author":"A.S. Rao","year":"1996","unstructured":"Rao, A.S.: AgentSpeak(L): BDI Agents Speak Out in a Logical Computable Language. In: Perram, J., Van de Velde, W. (eds.) MAAMAW 1996. LNCS, vol.\u00a01038, pp. 42\u201355. Springer, Heidelberg (1996)"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Visser, W., Havelund, K., Brat, G., Park, S.J.: Model checking programs. In: Proc. of the 15th IEEE International Conf. on Automated Software Engineering (2000)","DOI":"10.1109\/ASE.2000.873645"},{"key":"13_CR22","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1093\/logcom\/exi014","volume":"15","author":"M. Pauly","year":"2005","unstructured":"Pauly, M.: Programming and verifying subgame-perfect mechanisms. J. Log. Comput.\u00a015, 295\u2013316 (2005)","journal-title":"J. Log. Comput."},{"key":"13_CR23","unstructured":"Pauly, M., Wooldridge, M.: Logic for mechanism design\u2014a manifesto. In: GTDT 2003 workshop, Hakodate, Japan, AAMAS 2003 (2003)"},{"key":"13_CR24","unstructured":"Osman, N., Robertson, D.: Dynamic verification of trust in distributed open systems. In: IJCAI, pp. 1440\u20131445 (2007)"},{"key":"13_CR25","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"M.R.A. Huth","year":"2000","unstructured":"Huth, M.R.A., Ryan, M.D.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge (2000)"},{"key":"13_CR26","doi-asserted-by":"publisher","first-page":"927","DOI":"10.1109\/32.730543","volume":"24","author":"C. Heitmeyer","year":"1998","unstructured":"Heitmeyer, C., Kirby, J., Labaw, B., Archer, M., Bharadwaj, R.: Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Transactions on Software Engineering\u00a024, 927\u2013948 (1998)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR27","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1145\/337180.337234","volume-title":"Proceedings of the \u00a022nd\u00a0 International Conference on Software Engineering","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Zheng, H.: Bandera. In: Proceedings of the \u00a022nd\u00a0 International Conference on Software Engineering, pp. 439\u2013448. ACM Press, New York (2000)"},{"key":"13_CR28","unstructured":"Holzmann, G.J.: Personal communication (2008)"}],"container-title":["Lecture Notes in Computer Science","Declarative Agent Languages and Technologies VI"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-93920-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,23]],"date-time":"2023-05-23T05:11:25Z","timestamp":1684818685000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-93920-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783540939191","9783540939207"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-93920-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}