Lintao Zhang
RESEARCHER
.
I recently moved to Beijing to join MSR-Asia. Previously, I was 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 . My resume can be found here.
I prepared some material on SAT solving for a 3-day mini PhD course in IT-U of Copenhagen. If you want to learn about SAT solving, this should be a good starting point.
Publications
- John D. Davis and Lintao Zhang, FRP: a Nonvolatile Memory Research Platform Targeting NAND Flash, in The First Workshop on Integrating Solid-state Memory into the Storage Hierarchy, Held in Conjunction with ASPLOS 2009, Association for Computing Machinery, Inc., March 2009
- Manuel Costa, Jon Crowcroft, Miguel Castro, Antony Rowstron, Lidong Zhou, Lintao Zhang, and Paul Barham, Vigilante: End-to-End Containment of Internet Worm Epidemics, in ACM Transactions on Computer Systems, December 2008
- John D. Davis, Zhangxi Tan, Fang Yu, and Lintao Zhang, A Practical Reconfigurable Hardware Accelerator for Boolean Satisfiability Solvers, in 45th Design Automation Conference, Association for Computing Machinery, Inc., June 2008
- John D. Davis, Zhangxi Tan, Fang Yu, and Lintao Zhang, Designing an Efficient Hardware Implication Accelerator for SAT Solving, in International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer, Guangzhou, China, May 2008
- Wei Lin, Mao Yang, Lintao Zhang, and Lidong Zhou, PacificA: Replication in Log-Based Distributed Storage Systems, no. MSR-TR-2008-25, February 2008
- Manuel Costa, Miguel Castro, Lidong Zhou, Lintao Zhang, and Marcus Peinado, Bouncer: securing software by blocking bad input, in ACM Symposium on Operating Systems Principles (SOSP), Association for Computing Machinery, Inc., Stevenson, Washington, USA, October 2007
- Manuel Costa, Miguel Castro, Lidong Zhou, Lintao Zhang, and Marcus Peinado, Bouncer: securing software by blocking bad input, in ACM Symposium on Operating Systems Principles (SOSP), Association for Computing Machinery, Inc., October 2007
- Lucas Bordeaux and Lintao Zhang, A Solver for Quantified Boolean and Linear Constraints, in The 22nd Annual ACM Symposium on Applied Computing (SAC 2007), Seoul, Korea, March 2007
- Ilya Mironov and Lintao Zhang, Applications of SAT Solvers to Cryptanalysis of Hash Functions, in International Conference on Theory and Applications of Satisfiability Testing (SAT 06), Springer, Seattle, WA, August 2006
- Lintao Zhang, Solving QBF with Combined Conjunctive and Disjunctive Normal Form, in National Conference on Artificial Intelligence (AAAI), American Association for Artificial Intelligence , Boston, MA, July 2006
- Manuel Costa, Jon Crowcroft, Miguel Castro, Antony Rowstron, Lidong Zhou, Lintao Zhang, and Paul Barham, Stopping Internet Epidemics, in Proceedings of the International Zurich Seminar on Communications (IZS'06), February 2006
- Manuel Costa, Jon Crowcroft, Miguel Castro, Antony Rowstron, Lidong Zhou, Lintao Zhang, and Paul Barham, Vigilante: End-to-End Containment of Internet Worms, in ACM Symposium on Operating Systems Principles (SOSP), ACM Press, Birghton, UK, October 2005
- Lidong Zhou, Lintao Zhang, Frank McSherry, Nicole Immorlica, Manuel Costa, and Steve Chien, A First Look at Peer-to-Peer Worms: Threats and Defenses, in 4th International Workshop on Peer-To-Peer Systems (IPTPS '05), Ithaca, New York, USA, February 2005
- Thomas Ball, Byron Cook, Shuvendu K. Lahiri, and Lintao Zhang, Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement., in 16th International Conference on Computer Aided Verification (CAV 2004), Springer, Boston, MA, USA, July 2004
