1. SAT Competitions [Link]
   SAT Competitions are held to vote the best SAT solver.
2. CryptoMiniSat [GitHub] [soos.mate site]
   One of the winners in SAT Competition.
3. CryptoMiniSat 4.4 [Archive] CryptoMiniSat 2.9.6 [Archive]
   2.9.6 is the one we used in most of our papers.

1. Z3 [Link]

1. A Bit-Vector Solver with Word-Level Propagation [PDF]
2. A Bit-Vector Solver Based on Word-Level Propagation [Thesis] Available upon request.

1. X. Zhao, F. Zhang, T. Wang, S. Guo, Z. Shi, H. Liu, K. Ji. "MDASCA: An Enhanced Algebraic Side-Channel Attack for Error Tolerance and New Leakage Model Exploitation," In COSADE 2012, LNCS, vol. 7275, pp. 231-248, 2012.  [PDF] (Best Paper Award)
2. S. Guo, X. Zhao, F. Zhang*, T. Wang, Z. Shi, F. -X Standaert, "Exploiting the Incomplete Diffusion Feature: A Specialized Analytical Side-Channel Attack against the AES and its Application to Microcontroller Implementations," IEEE Transactions on Information Forensics & Security, Vol.9, No.6, pp.999-1014, 2014. (CCF-A, IF=4.332) [PDF]
3. X. Zhao, S. Guo, F. Zhang*, T. Wang, Z. Shi, Z. Liu, J. Gallais, "A Comprehensive Study of Multiple Deductions-based Algebraic Trace Driven Cache Attacks on AES," Computers & Security, Vol.39: 173-189, 2013. [PDF]

1. F. Zhang*, S. Guo, X. Zhao, T. Wang, J. Yang, F. -X. Standaert, D. Gu "A Framework for the Analysis and Evaluation of Algebraic Fault Attacks on Lightweight Block Ciphers," IEEE Transactions on Information Forensics & Security, Vol.11, No.5, pp.1039-1054, 2016.  (CCF-A, IF=4.332) [PDF]
2. I have a lot of publications about the algebraic fault analysis technique. Please check my fulllist of publications [PDF]

with a hardware solver using FPGA

1. Pre-Silicon Security Verification and Validation: A Formal Perspective [PDF]
2. Eliminating the Hardware-Software Boundary: A Proof-Carrying Approach for Trust Evaluation on Computer Systems [PDF]
3. AppSAT: Approximately Deobfuscating Integrated Circuits [PDF] HOST2017 Best paper.
4. PCH Framework for IP Runtime Security Verification [PDF]
5. Cyclic Obfuscation for Creating SAT-Unresolvable Circuits [PDF]

1. Automatic Enumeration of (Related-key) Differential and Linear Characteristics with Predefined Properties [PDF]
2. Automatic Security Evaluation and (Related-key) Differential Characteristic Search: Application to SIMON, PRESENT, LBlock, DES(L) and Other Bit-oriented Block Ciphers [PDF]
   Siwei's paper in Asiacrypt 2014.
3. Automatic Security Evaluation of Block Ciphers with S-bP Structures Against Related-Key Differential Attacks [PDF]
   Siwei's paper in Inscrypt 2013.
4. Improved Linear (hull) Cryptanalysis of Round-reduced Versions of KATAN, 2015 [PDF]
5. Improved Linear (hull) Cryptanalysis of Round-reduced Versions of SIMON, 2015 [PDF]
6. MILP-Based Automatic Search Algorithms for ARX for Differential and Linear Trails for Speck.[PDF]
   Siwei's paper in FSE2016.
7. Mixed Integer Programming Models for Finite Automaton and Its Application to Additive Differential Patterns of Exclusive-Or, 2016 [PDF]

1. Differential Fault Analysis Automation, 2017[PDF] Debdeep's paper on eprint.
2. Automated Fault Analysis of Assembly Code With a Case Study on PRESENT Implementation, 2017[PDF] Jakub's paper on eprint.
3. AutoFault: towards automatic construction of algebraic fault attacks, 2017[PDF] autmatioed AFA paper on FTDC.