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, IACR International Conference on the Theory and Applications of Cryptographic Techniques (EUROCRYPT), 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

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.1137/1.9781611973082.58
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.193.9148

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.

D. A. Naumann, Theory for software verification, 2009.

N. Nisan, T. Roughgarden, E. Tardos, and V. V. Vazirani, Algorithmic game theory, 2007.
DOI : 10.1017/CBO9780511800481

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.

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, 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.

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

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, 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

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

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.