{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:19:32Z","timestamp":1763468372297,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662541098"},{"type":"electronic","value":"9783662541104"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-54110-4_20","type":"book-chapter","created":{"date-parts":[[2016,12,10]],"date-time":"2016-12-10T08:48:58Z","timestamp":1481359738000},"page":"279-293","source":"Crossref","is-referenced-by-count":8,"title":["Computer-Aided Verification for Mechanism Design"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emilio Jes\u00fas Gallego","family":"Arias","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aaron","family":"Roth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,12,11]]},"reference":[{"key":"20_CR1","unstructured":"Barrett, C., Sebastini, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of satisfiability, vol. 185. IOS press (2009)"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-22792-9_5","volume-title":"Advances in Cryptology \u2013 CRYPTO 2011","author":"G Barthe","year":"2011","unstructured":"Barthe, G., Gr\u00e9goire, B., Heraud, S., B\u00e9guelin, S.Z.: Computer-aided security proofs for the working cryptographer. In: Rogaway, P. (ed.) CRYPTO 2011. LNCS, vol. 6841, pp. 71\u201390. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22792-9_5"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-10082-1_6","volume-title":"Foundations of Security Analysis and Design VII","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Dupressoir, F., Gr\u00e9goire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146\u2013166. Springer, Heidelberg (2014). doi: 10.1007\/978-3-319-10082-1_6"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gaboardi, M., Gallego Arias, E.J., Hsu, J., Roth, A., Strub, P.-Y.: Higher-order approximate relational refinement types for mechanism design and differential privacy. In: ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Mumbai, India, pp. 55\u201368 (2015). http:\/\/arxiv.org\/abs\/1407.6845","DOI":"10.1145\/2676726.2677000"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/11761679_25","volume-title":"Advances in Cryptology - EUROCRYPT 2006","author":"M Bellare","year":"2006","unstructured":"Bellare, M., Rogaway, P.: The security of triple encryption and a framework for code-based game-playing proofs. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol. 4004, pp. 409\u2013426. Springer, Heidelberg (2006). doi: 10.1007\/11761679_25"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Br\u00e2nzei, S., Procaccia, A.D.: Verifiably truthful mechanisms. In: ACM SIGACT Innovations in Theoretical Computer Science (ITCS), Princeton, New Jersey (2014)","DOI":"10.1145\/2688073.2688098"},{"key":"20_CR7","unstructured":"Caminati, M.B., Kerber, M., Lange, C., Rowat, C.: Sound auction specification and implementation. In: ACM SIGecom Conference on Economics and Computation (EC), Portland, Oregon, pp. 547\u2013564 (2015). http:\/\/doi.acm.org\/10.1145\/2764468.2764511"},{"key":"20_CR8","unstructured":"Christodoulou, G., Koutsoupias, E.: The price of anarchy of finite congestion games. In: ACM SIGACT Symposium on Theory of Computing (STOC), Baltimore, Maryland, pp. 67\u201373. ACM (2005). http:\/\/dl.acm.org\/citation.cfm?id=1060600"},{"issue":"1","key":"20_CR9","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/BF01726210","volume":"11","author":"EH Clarke","year":"1971","unstructured":"Clarke, E.H.: Multipart pricing of public goods. Public Choice 11(1), 17\u201333 (1971)","journal-title":"Public Choice"},{"key":"20_CR10","unstructured":"Conitzer, V.: Computational aspects of preference aggregation. PhD thesis, IBM (2006)"},{"key":"20_CR11","unstructured":"Conitzer, V., Sandholm, T.: Complexity of mechanism design. In: Conference on Uncertainty in Artificial Intelligence (UAI), Edmonton, Alberta, pp. 103\u2013110. Morgan Kaufmann Publishers Inc. (2002)"},{"issue":"1","key":"20_CR12","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1137\/070699652","volume":"39","author":"C Daskalakis","year":"2009","unstructured":"Daskalakis, C., Goldberg, P.W., Papadimitriou, C.H.: The complexity of computing a Nash equilibrium. SIAM J. Comput. 39(1), 195\u2013259 (2009)","journal-title":"SIAM J. Comput."},{"issue":"2","key":"20_CR13","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1016\/j.geb.2006.02.003","volume":"55","author":"AV Goldberg","year":"2006","unstructured":"Goldberg, A.V., Hartline, J.D., Karlin, A.R., Saks, M., Wright, A.: Competitive auctions. Games Econ. Behav. 55(2), 242\u2013269 (2006)","journal-title":"Games Econ. Behav."},{"issue":"4","key":"20_CR14","first-page":"617","volume":"41","author":"T Groves","year":"1973","unstructured":"Groves, T.: Incentives in teams. Econ. J. Econ. Soc. 41(4), 617\u2013631 (1973)","journal-title":"Econ. J. Econ. Soc."},{"key":"20_CR15","unstructured":"Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005\/181 (2005). https:\/\/eprint.iacr.org\/2005\/181.pdf"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Hart, S., Mansour, Y.: The communication complexity of uncoupled Nash equilibrium procedures. In: ACM SIGACT Symposium on Theory of Computing (STOC), San Diego, California, pp. 345\u2013353. ACM (2007)","DOI":"10.1145\/1250790.1250843"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Hartline, J.D., Kleinberg, R., Malekian, A.: Bayesian incentive compatibility via matchings. In: ACM-SIAM Symposium on Discrete Algorithms (SODA), San Francisco, California, pp. 734\u2013747. SIAM (2011)","DOI":"10.1137\/1.9781611973082.58"},{"key":"20_CR18","unstructured":"Kerber, M., Lange, C., Rowat, C.: An introduction to mechanized reasoning. CoRR, abs\/1603.02478, 2016. http:\/\/arxiv.org\/abs\/1603.02478"},{"key":"20_CR19","doi-asserted-by":"crossref","unstructured":"Li, S.: Obviously strategy-proof mechanisms. SSRN Electron. J. http:\/\/dx.doi.org\/10.2139\/ssrn.2560028","DOI":"10.2139\/ssrn.2560028"},{"key":"20_CR20","unstructured":"Milgrom, P., Segal, I.: Deferred acceptance auctions and radio spectrum reallocation (2014). http:\/\/www.as.huji.ac.il\/sites\/default\/files\/DA%20Heuristic%20Auctions%20June-2014.pdf"},{"key":"20_CR21","unstructured":"Mu\u2019alem, A.: A note on testing truthfulness. In: Electronic Colloquium on Computational Complexity (ECCC), No. 130 (2005)"},{"key":"20_CR22","volume-title":"Selfish Routing and the Price of Anarchy","author":"T Roughgarden","year":"2005","unstructured":"Roughgarden, T.: Selfish Routing and the Price of Anarchy, vol. 174. MIT Press, Cambridge (2005)"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-45193-8_2","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"T Sandholm","year":"2003","unstructured":"Sandholm, T.: Automated mechanism design: a new application area for search algorithms. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 19\u201336. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45193-8_2"},{"issue":"1","key":"20_CR24","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1111\/j.1540-6261.1961.tb02789.x","volume":"16","author":"W Vickrey","year":"1961","unstructured":"Vickrey, W.: Counterspeculation, auctions, and competitive sealed tenders. J. Finan. 16(1), 8\u201337 (1961)","journal-title":"J. Finan."}],"container-title":["Lecture Notes in Computer Science","Web and Internet Economics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-54110-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,16]],"date-time":"2019-09-16T07:47:51Z","timestamp":1568620071000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-54110-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662541098","9783662541104"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-54110-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}