C. Barrett, R. Sebastini, S. A. Seshia, and C. Tinelli, Satisfiability modulo theories, Handbook of satisfiability, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01095009

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computer-Aided Security Proofs for the Working Cryptographer, IACR International Cryptology Conference (CRYPTO), pp.71-90, 2011.
DOI : 10.1007/978-3-642-22792-9_5

URL : https://hal.archives-ouvertes.fr/hal-01112075

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., EasyCrypt: A Tutorial, Foundations of Security Analysis and Design VII -FOSAD 2012/2013 Tutorial Lectures, pp.146-166, 2014.
DOI : 10.1007/978-3-642-22792-9_5

URL : https://hal.archives-ouvertes.fr/hal-01114366

G. Barthe, M. Gaboardi, E. J. Gallego-arias, J. Hsu, A. Roth et al., Higher-order approximate relational refinement types for mechanism design and differential privacy, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.55-68, 2015.
DOI : 10.1145/2775051.2677000

URL : http://arxiv.org/abs/1407.6845

M. Bellare and P. Rogaway, The Security of Triple Encryption and a Framework??for??Code-Based??Game-Playing??Proofs, Lecture Notes in Computer Science, vol.4004, pp.409-426, 2006.
DOI : 10.1007/11761679_25

S. Brânzei and A. D. Procaccia, Verifiably Truthful Mechanisms, Proceedings of the 2015 Conference on Innovations in Theoretical Computer Science, ITCS '15
DOI : 10.1145/2688073.2688098

M. B. Caminati, M. Kerber, C. Lange, and C. Rowat, Sound auction specification and implementation, ACM SIGecom Conference on Economics and Computation (EC), pp.547-564, 2015.
DOI : 10.1145/2764468.2764511

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.696.5096

G. Christodoulou and E. Koutsoupias, The price of anarchy of finite congestion games, Proceedings of the thirty-seventh annual ACM symposium on Theory of computing , STOC '05, pp.67-73, 2005.
DOI : 10.1145/1060590.1060600

E. H. Clarke, Multipart pricing of public goods, Public Choice, vol.7, issue.1, pp.17-33, 1971.
DOI : 10.1007/BF01726210

V. Conitzer, Computational aspects of preference aggregation, IBM, 2006.

V. Conitzer and T. Sandholm, Complexity of mechanism design, Conference on Uncertainty in Artificial Intelligence (UAI), pp.103-110, 2002.

C. Daskalakis, P. W. Goldberg, and C. H. Papadimitriou, The Complexity of Computing a Nash Equilibrium, SIAM Journal on Computing, vol.39, issue.1, pp.195-259, 2009.
DOI : 10.1137/070699652

A. V. Goldberg, J. D. Hartline, A. R. Karlin, M. Saks, and A. Wright, Competitive auctions, Games and Economic Behavior, vol.55, issue.2, pp.242-269, 2006.
DOI : 10.1016/j.geb.2006.02.003

B. Gross, M. Dearmond, and P. Denice, Common enrollment, parents, and school choice: Early evidence from denver and new orleans. making school choice work series, Center on Reinventing Public Education (CRPE), 2015.

T. Groves, Incentives in Teams, Econometrica, vol.41, issue.4, pp.617-631, 1973.
DOI : 10.2307/1914085

S. Halevi, A plausible approach to computer-aided cryptographic proofs, Cryptology ePrint Archive Report, vol.181, 2005.

S. Hart and Y. Mansour, The communication complexity of uncoupled nash equilibrium procedures, Proceedings of the thirty-ninth annual ACM symposium on Theory of computing , STOC '07, pp.345-353, 2007.
DOI : 10.1145/1250790.1250843

J. D. Hartline, R. Kleinberg, and A. Malekian, Bayesian incentive compatibility via matchings, ACM?SIAM Symposium on Discrete Algorithms (SODA), pp.734-747, 2011.
DOI : 10.1016/j.geb.2015.02.002

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.193.9148

A. Hassidim, D. Marciano-romm, A. Romm, and R. I. Shorrer, strategic behavior' in a strategy-proof environment. Working paper, 2016.

M. Kerber, C. Lange, and C. Rowat, An introduction to mechanized reasoning. CoRR, abs, 1603.
DOI : 10.1016/j.jmateco.2016.06.005

URL : http://doi.org/10.1016/j.jmateco.2016.06.005

S. Li, Obviously Strategy-Proof Mechanisms, SSRN Electronic Journal
DOI : 10.2139/ssrn.2560028

P. Milgrom and I. Segal, Deffered acceptance auctions and radio spectrum reallocation, 2014.
DOI : 10.1145/2600057.2602834

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.473.8144

A. Mu, A note on testing truthfulness, Electronic Colloquium on Computational Complexity (ECCC), number 130, 2005.

T. Roughgarden, Selfish Routing and the Price of Anarchy, 2005.
DOI : 10.1017/CBO9781316779309.012

T. Sandholm, Automated Mechanism Design: A New Application Area for Search Algorithms, International Conference on Principles and Practice of Constraint Programming (CP), pp.19-36, 2003.
DOI : 10.1007/978-3-540-45193-8_2

W. Vickrey, COUNTERSPECULATION, AUCTIONS, AND COMPETITIVE SEALED TENDERS, The Journal of Finance, vol.16, issue.1, pp.8-37, 1961.
DOI : 10.1111/j.1540-6261.1961.tb02789.x

]. R. References1, T. A. Alur, O. Henzinger, and . Kupferman, Alternating-time temporal logic, Journal of the ACM, vol.49, issue.5, pp.672-713, 2002.

W. Bai, E. M. Tadjouddine, T. R. Payne, and S. Guan, A Proof-Carrying Code Approach to Certificate Auction Mechanisms, FACS, pp.23-40, 2013.
DOI : 10.1007/978-3-319-07602-7_4

G. Barthe, B. Grégoire, and S. Zanella-béguelin, Formal certification of code-based cryptographic proofs, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), 2009.
DOI : 10.1145/1480881.1480894

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.220.4653

G. Barthe, F. Dupressoir, B. Grégoire, C. Kunz, B. Schmidt et al., EasyCrypt: A Tutorial, Foundations of Security Analysis and Design VII -FOSAD 2012/2013 Tutorial Lectures, pp.146-166, 2014.
DOI : 10.1007/978-3-642-22792-9_5

URL : https://hal.archives-ouvertes.fr/hal-01114366

G. Barthe, M. Gaboardi, E. J. Gallego-arias, J. Hsu, A. Roth et al., Higher-order approximate relational refinement types for mechanism design and differential privacy, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.55-68, 2015.
DOI : 10.1145/2775051.2677000

URL : http://arxiv.org/abs/1407.6845

N. Benton, Simple relational correctness proofs for static analyses and program transformations, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.14-25, 2004.
DOI : 10.1145/964001.964003

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.4900

R. Chadha, L. Cruz-filipe, P. Mateus, and A. Sernadas, Reasoning about probabilistic sequential programs, Theoretical Computer Science, vol.379, issue.1-2, pp.142-165, 2007.
DOI : 10.1016/j.tcs.2007.02.040

URL : http://doi.org/10.1016/j.tcs.2007.02.040

E. H. Clarke, Multipart pricing of public goods, Public Choice, vol.7, issue.1, pp.17-33, 1971.
DOI : 10.1007/BF01726210

S. Cook, Soundness and Completeness of an Axiom System for Program Verification, SIAM Journal on Computing, vol.7, issue.1, pp.70-90, 1978.
DOI : 10.1137/0207005

C. Flanagan and J. B. Saxe, Avoiding exponential explosion: Generating compact verification conditions, ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages (POPL), pp.193-205, 2001.

R. W. Floyd, Assigning meanings to programs, Symposium on Applied Mathematics. Amer, 1967.
DOI : 10.1007/978-94-011-1793-7_4

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A machinechecked proof of the odd order theorem, Interactive Theorem Proving (ITP), pp.163-179, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00816699

T. Groves, Incentives in Teams, Econometrica, vol.41, issue.4, pp.617-631, 1973.
DOI : 10.2307/1914085

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, 1969.
DOI : 10.1007/978-94-011-1793-7_5

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.2392

D. Kozen, A probabilistic PDL, Proceedings of the fifteenth annual ACM symposium on Theory of computing , STOC '83, 1985.
DOI : 10.1145/800061.808758

URL : http://doi.org/10.1016/0022-0000(85)90012-1

A. Lapets, A. Levin, and D. Parkes, A Typed Truthful Language for One-dimensional Truthful Mechanism Design, 2008.

C. Morgan, A. Mciver, and K. Seidel, Probabilistic predicate transformers, ACM Transactions on Programming Languages and Systems, vol.18, issue.3, pp.325-353, 1996.
DOI : 10.1145/229542.229547

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.166.127

A. Mu-'alem and N. Nisan, Truthful approximation mechanisms for restricted combinatorial auctions, Games and Economic Behavior, vol.64, issue.2, pp.612-631, 2008.
DOI : 10.1016/j.geb.2007.12.009

E. M. Tadjouddine and F. Guerin, Verifying Dominant Strategy Equilibria in Auctions, CEEMAS 2007, pp.288-297, 2007.
DOI : 10.1007/978-3-540-75254-7_29

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.7128

E. M. Tadjouddine, F. Guerin, and W. Vasconcelos, Abstracting and Verifying Strategy-Proofness for Auction Mechanisms, Declarative Agent Languages and Technologies VI, pp.197-214, 2009.
DOI : 10.1109/32.730543

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.140.9737

A. M. Turing, Checking a large routine, Report on a Conference on High Speed Automatic Computation, pp.67-69, 1949.

W. Vickrey, COUNTERSPECULATION, AUCTIONS, AND COMPETITIVE SEALED TENDERS, The Journal of Finance, vol.16, issue.1, pp.8-37, 1961.
DOI : 10.1111/j.1540-6261.1961.tb02789.x

M. Wooldridge, T. Agotnes, P. E. Dunne, and W. Van-der-hoek, Logic for automated mechanism design?A progress report, AAAI Conference on Artificial Intelligence, pp.9-17, 2007.