You could start by quickly browsing through the huge list of papers that cite Z3 [1]. Microsoft uses Z3 extensively for bug finding for all sort of products, n

You could start by quickly browsing through the huge list of papers that cite Z3 [1]. Microsoft uses Z3 extensively for bug finding for all sort of products, notably through the SAGE tool. There is a great write up on its impact. [2] From that paper: "Finding all these bugs has saved millions of dollars to Microsoft, as well as to the world in time and energy, by avoiding expensive security patches to more than 1 billion PCs. The software running on your PC has been affected by SAGE. Since 2008, SAGE has been running 24/7 on an average of 100-plus machines/cores automatically fuzzing hundreds of applications in Microsoft security testing labs. This is more than 300 machine- years and the largest computational usage ever for any SMT (Satisfiability Modulo Theories) solver, with more than 1 billion constraints processed to date. SAGE is so effective at finding bugs that, for the first time, we faced “bug triage” issues with dynamic test generation." [1] http://scholar.google.com/scholar?cites=4828743947843773221&as_sdt=5,33&sciodt=1,33 http://scholar.google.com/scholar?cites=4828743947843773221&... [2] http://dl.acm.org/citation.cfm?id=2094081 http://dl.acm.org/citation.cfm?id=2094081