Lintao Zhang Researcher Microsoft Research Silicon Valley 1065 La Avenida Mountain View, CA 94043 Email: lintaoz at microsoft dot com Tel. +1 650.693.3815

I am a researcher at Microsoft Research Silicon Valley. I work on a diverse set of exciting projects on verification and logic, distributed systems, storage, computer architecture and reconfigurable computing.

My Ph.D. thesis can be downloaded here .

I prepared some material about SAT solving for a 3-day mini PhD course in IT-U of Copenhagen. If you want to learn about SAT solving, it whould be a good starting point.

The executable for QBF solver IQTest (see the paper published in AAAI 2006) is available here .

Publications

• J. Davis, Z. Tan, F. Yu and L. Zhang, "A Practical Reconfigurable Hardware Accelerator for Boolean Satisfiability Solvers", 45th Design Automation Conference (DAC2008), Anaheim, CA, June, 2008 [PDF]
• J. Davis, Z. Tan, F. Yu and L. Zhang, "Designing an Efficient Hardware Implication Accelerator for SAT Solving ", Eleventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2008), Guangzhou, China, May, 2008 [PDF]
• M. Costa, M. Castro, L. Zhou, L. Zhang and M. Peinado, " Bouncer: securing software by blocking bad input", 20th ACM Symposium on Operating Systems Principles (SOSP2007), Stevenson, WA, Oct. 2007 [PDF]
• L. Bordeaux and L. Zhang, "A solver for Quantified Boolean and Linear Constraints", The 22nd Annual ACM Symposium on Applied Computing (SAC 2007), Seoul, Korea, March 2007 [PDF]
• L. Bordeaux, Y. Hamadi and L. Zhang, "Propositional Satisfiability and Constraint Programming: A Comparative Survey", ACM Surveys, 38(4), 2006 [PDF]
• L. Zhang, "Solving QBF with Combined Conjunctive and Disjunctive Normal Form", Twenty-First National Conference on Artificial Intelligence (AAAI 2006), Boston, MA, July 2006 [PDF]
• I. Mironov, L. Zhang "Applications of SAT Solvers to Cryptanalysis of Hash Functions", Nineth International Conference on Theory and Applications of Satisfiability Testing (SAT 2006), Seattle, WA, August, 2006 [PDF]
• M. Costa, J. Crowcroft, M. Castro, A. Rowstron, L. Zhou, L. Zhang and P. Barham, "Vigilante: End-to-End Containment of Internet Worms", 20th ACM Symposium on Operating Systems Principles (SOSP2005), Brighton, United Kingdom, October, 2005 [PDF]
• D. Marinov, S. Khurshid, S. Bugrara, L. Zhang and M. Rinard, "Optimizations for Compiling Declarative Models into Boolean Formulas", Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT2005), St. Andrews, United Kingdom, June 2005 [PDF]
• L. Zhang, "On Subsumption Removal and On-the-Fly CNF Simplification", Eighth International Conference on Theory and Applications of Satisfiability Testing (SAT 2005), St. Andrews, United Kingdom, June 2005 [PDF]
• L. Zhou, L. Zhang, F. McSherry, N. Immorlica, M. Costa and S Chien, "A First Look at Peer-to-Peer Worms: Threats and Defenses", 4th International Workshop on Peer-To-Peer Systems (IPTPS'05), Ithaca, NY, Feb. 2005 [PDF]
• T. Ball, B. Cook, S. K. Lahiri and L. Zhang, "Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement", 16th International Conference on Computer Aided Verification (CAV2004), Boston, MA, July, 2004 [PDF]
• L. Zhang and S. Malik, "Cache Performance of SAT Solvers: A Case Study for Efficient Implementation of Algorithms", Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT2003), S. Margherita Ligure - Portofino ( Italy), May 5-8 2003 [PDF]
• L. Zhang and S. Malik, "Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formulas", Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT2003), S. Margherita Ligure - Portofino ( Italy), May 5-8 2003 [PDF]
• L. Zhang and S. Malik, "Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications", Proceedings of Design, Automation and Test in Europe (DATE2003). Munich, Germany, March 2003 [PDF] [Best Paper Award]
• L. Zhang and S. Malik, "Towards Symmetric Treatment of Conflicts And Satisfaction in Quantified Boolean Satisfiability Solver", Proceedings of 8th International Conference on Principles and Practice of est Paper Award WinnerConstraint Programming (CP2002). Ithaca, NY, Sept. 2002. [PDF]
• L. Zhang and S. Malik, "Conflict Driven Learning in a Quantified Boolean Satisfiability Solver", Proceedings of International Conference on Computer Aided Design (ICCAD2002), San Jose, CA, Nov. 2002. [PDF]
• L. Zhang and S. Malik, "The Quest for Efficient Boolean Satisfiability Solvers", Invited Paper, Proceedings of 8th International Conference on Computer Aided Deduction(CADE 2002) and also in Proceedings of 14th Conference on Computer Aided Verification (CAV2002), Copenhagen, Denmark, July 2002 [PDF]
• M. Ganai, L. Zhang, P. Ashar, A. Gupta and S. Malik, "Combining Strengths of Circuit-based and CNF-based Algorithms for a High-Performance SAT Solver", Proceedings of 39th Design Automation Conference(DAC2002), June, 2002 [PDF]
• A. Gupta, Z. Yang, P. Ashar, L. Zhang and S. Malik, "Partition Based Decision Heuristics for Image Computation Using SAT and BDDs", Proceedings of International Conference on Computer Aided Design (ICCAD2001), San Jose, CA, Nov. 2001 [PDF]
• L. Zhang, C. Madigan, M. Moskewicz and S. Malik, "Efficient Conflict Driven Learning in a Boolean Satisfiability Solver", Proceedings of International Conference on Computer Aided Design (ICCAD2001), San Jose, CA, Nov. 2001 [PDF]
• M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik, "Chaff: Engineering an Efficient SAT Solver", 38th Design Automation Conference (DAC2001), Las Vegas, June 2001. [PDF]