R. Alur, R. Bodík, G. Juniwal, M. M. Martin, M. Raghothaman et al., Syntax-guided synthesis, 2013 Formal Methods in Computer-Aided Design, pp.1-17, 2013.
DOI : 10.1109/FMCAD.2013.6679385
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.377.2829

R. J. Anderson and M. G. Kuhn, Low cost attacks on tamper resistant devices, Security Protocols Workshop, pp.125-136, 1997.
DOI : 10.1007/BFb0028165

A. Barenghi, G. Bertoni, A. Palomba, and R. Susella, A novel fault attack against ECDSA, 2011 IEEE International Symposium on Hardware-Oriented Security and Trust, pp.161-166, 2011.
DOI : 10.1109/HST.2011.5955015

A. Barenghi, G. M. Bertoni, L. Breveglieri, and G. Pelosi, A fault induction technique based on voltage underfeeding with application to attacks against AES and RSA, Journal of Systems and Software, vol.86, issue.7, pp.1864-1878, 2013.
DOI : 10.1016/j.jss.2013.02.021

G. Barthe, J. M. Crespo, S. Gulwani, C. Kunz, and M. Marron, From relational verification to SIMD loop synthesis, PPOPP, pp.123-134, 2013.

G. Barthe, F. Dupressoir, P. Fouque, B. Grégoire, M. Tibouchi et al., Making RSA-PSS provably secure against non-random faults. Cryptology ePrint Archive, 2014.
DOI : 10.1007/978-3-662-44709-3_12
URL : https://hal.archives-ouvertes.fr/hal-01094057

G. Barthe, F. Dupressoir, P. Fouque, B. Gregoire, and J. Zapalowicz, Synthesis of Fault Attacks on Cryptographic Implementations, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS '14, 2014.
DOI : 10.1145/2660267.2660304
URL : https://hal.archives-ouvertes.fr/hal-01094034

G. Barthe, B. Grégoire, S. Heraud, and S. Z. Béguelin, Computer-Aided Security Proofs for the Working Cryptographer, LNCS, vol.6841, pp.71-90, 2011.
DOI : 10.1007/978-3-642-22792-9_5
URL : https://hal.archives-ouvertes.fr/hal-01112075

A. Bauer, E. Jaulmes, E. Prouff, and J. Wild, Horizontal collision correlation attack on elliptic curves, Selected Areas in Cryptology, 2013.
DOI : 10.1007/s12095-014-0111-8

A. G. Bayrak, F. Regazzoni, D. Novo, and P. Ienne, Sleuth: Automated Verification of Software Power Analysis Countermeasures, Cryptographic Hardware and Embedded Systems-CHES 2013, pp.293-310
DOI : 10.1007/978-3-642-40349-1_17

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

I. Biehl, B. Meyer, and V. Müller, Differential Fault Attacks on Elliptic Curve Cryptosystems, LNCS, vol.1880, pp.131-146, 2000.
DOI : 10.1007/3-540-44598-6_8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.107.3920

D. Boneh, R. A. Demillo, and R. J. Lipton, On the importance of checking cryptographic protocols for faults (extended abstract), LNCS, vol.1233, issue.97, pp.37-51, 1997.

E. Brier, D. Naccache, P. Q. Nguyen, and M. Tibouchi, Modulus fault attacks against RSA-CRT signatures, CHES 2011, pp.192-206
DOI : 10.1007/978-3-642-23951-9_13
URL : https://hal.archives-ouvertes.fr/hal-01109981

M. Christofi, B. Chetali, L. Goubin, and D. Vigilant, Formal verification of a CRT-RSA implementation against fault attacks, Journal of Cryptographic Engineering, vol.2009, issue.3, pp.157-167, 2013.
DOI : 10.1007/s13389-013-0049-3

M. Ciet and M. Joye, Elliptic curve cryptosystems in the presence of permanent and transient faults. Designs, Codes and Cryptography, pp.33-43, 2005.

H. Eldib and C. Wang, Synthesis of Masking Countermeasures against Side Channel Attacks, Computer Aided Verification (CAV'14, 2014.
DOI : 10.1007/978-3-319-08867-9_8

H. Eldib, C. Wang, and P. Schaumont, SMT-Based Verification of Software Countermeasures against Side-Channel Attacks, Tools and Algorithms for the Construction and Analysis of Systems, pp.62-77, 2014.
DOI : 10.1007/978-3-642-54862-8_5

P. Fouque, N. Guillermin, D. Leresteux, M. Tibouchi, and J. Zapalowicz, Attacking RSA-CRT signatures with faults on montgomery multiplication, CHES 2012, pp.447-462, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01094316

P. Fouque, D. Leresteux, and F. Valette, Using faults for buffer overflow effects, Proceedings of the 27th Annual ACM Symposium on Applied Computing, SAC '12, pp.1638-1639, 2012.
DOI : 10.1145/2245276.2232038

P. Fouque, G. Martinet, and G. Poupard, Attacking Unbalanced RSA-CRT Using SPA, CHES 2003, pp.254-268
DOI : 10.1007/978-3-540-45238-6_21
URL : https://hal.archives-ouvertes.fr/inria-00563969

N. Gama and P. Q. Nguyen, Predicting Lattice Reduction, LNCS, vol.4965, pp.31-51, 2008.
DOI : 10.1007/978-3-540-78967-3_3

S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan, Synthesis of loop-free programs, PLDI, 2011.

S. Jha, S. Gulwani, S. Seshia, and A. Tiwari, Oracle-guided component-based program synthesis, Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, ICSE '10, 2010.
DOI : 10.1145/1806799.1806833

M. Joye, A. K. Lenstra, and J. Quisquater, Chinese Remaindering Based Cryptosystems in the Presence of Faults, Journal of Cryptology, vol.12, issue.4, pp.241-245, 1999.
DOI : 10.1007/s001459900055

J. C. Lagarias, The computational complexity of simultaneous diophantine approximation problems, 23rd FOCS, pp.32-39, 1982.

C. , L. Goues, S. Forrest, and W. Weimer, Current challenges in automatic software repair, Software Quality Jornal, vol.21, pp.421-443, 2013.

C. , L. Goues, T. Nguyen, S. Forrest, and W. Weimer, Genprog: A generic method for automatic software repair, IEEE Transactions on Software Engineering, vol.38, pp.54-72, 2012.

A. Lenstra, H. Lenstra, and L. Lovász, Factoring polynomials with rational coefficients, Mathematische Annalen, vol.32, issue.4, pp.515-534, 1982.
DOI : 10.1007/BF01457454

D. Maimut, C. Murdica, D. Naccache, and M. Tibouchi, Fault Attacks on Projective-to-Affine Coordinates Conversion, In COSADE, pp.46-61, 2013.
DOI : 10.1007/978-3-642-40026-1_4
URL : https://hal.archives-ouvertes.fr/hal-00857190

P. L. Montgomery, Modular multiplication without trial division, Mathematics of Computation, vol.44, issue.170, pp.519-521, 1985.
DOI : 10.1090/S0025-5718-1985-0777282-X

N. Moro, K. Heydemann, E. Encrenaz, and B. Robisson, Formal verification of a software countermeasure against instruction skip attacks, Journal of Cryptographic Engineering, vol.100, issue.11, pp.1-12, 2014.
DOI : 10.1007/s13389-014-0077-7
URL : https://hal.archives-ouvertes.fr/emse-00869509

A. Moss, E. Oswald, D. Page, and M. Tunstall, Compiler Assisted Masking, CHES, pp.58-75, 2012.
DOI : 10.1007/978-3-642-33027-8_4
URL : http://urn.kb.se/resolve?urn=urn:nbn:se:bth-7057

C. Murdica, Physical Security of Elliptic Curve Cryptography, 2014.
URL : https://hal.archives-ouvertes.fr/tel-01179584

D. Naccache, P. Q. Nguyen, M. Tunstall, and C. Whelan, Experimenting with Faults, Lattices and the DSA, PKC 2005, pp.16-28, 2005.
DOI : 10.1007/978-3-540-30580-4_3

P. Q. Nguyen and J. Stern, Merkle-Hellman revisited: A cryptanalysis of the Qu-Vanstone cryptosystem based on group factorizations, CRYPTO'97, pp.198-212, 1997.
DOI : 10.1007/BFb0052236

P. Q. Nguyen and J. Stern, Lattice Reduction in Cryptology: An Update, ANTS, pp.85-112, 2000.
DOI : 10.1007/10722028_4

D. Page and F. Vercauteren, Fault and side-channel attacks on pairing based cryptography, Cryptology ePrint Archive Report, vol.283283, 2004.

P. Rauzy and S. Guilley, A formal proof of countermeasures against fault injection attacks on CRT-RSA, Journal of Cryptographic Engineering, vol.21, issue.2, pp.1-13, 2013.
DOI : 10.1007/s13389-013-0065-3
URL : https://hal.archives-ouvertes.fr/hal-00863914

J. Schmidt and M. Medwed, A Fault Attack on ECDSA, 2009 Workshop on Fault Diagnosis and Tolerance in Cryptography (FDTC), pp.93-99, 2009.
DOI : 10.1109/FDTC.2009.38

C. Schnorr and M. Euchner, Lattice basis reduction: Improved practical algorithms and solving subset sum problems, Mathematical Programming, vol.13, issue.1, pp.181-199, 1994.
DOI : 10.1007/BF01581144

A. Solar-lezama, R. M. Rabbah, R. Bodík, and K. Ebcioglu, Programming by sketching for bit-streaming programs, PLDI, 2005.

S. Srivastava, S. Gulwani, and J. S. Foster, From program verification to program synthesis, POPL, 2010.

W. Stein, The Sage Development Team, Sage Mathematics Software, 2012.

Y. Wei, Y. Pei, C. A. Furia, L. S. Silva, S. Buchholz et al., Automated fixing of programs with contracts, Proceedings of the 19th international symposium on Software testing and analysis, ISSTA '10, pp.61-72, 2010.
DOI : 10.1145/1831708.1831716