avatar

Nathan Wetzler, Ph.D.
Postdoctoral Fellow at The University of Texas at Austin

About Me

I recently completed a doctoral degree in Computer Sciences at The University of Texas at Austin. My focus has been on using formal verification to increase confidence in satisfiability solvers.

My colleagues and I developed a method for efficiently checking the results for all contemporary satisfiability solvers.

Education

  • 2015

    Doctor of Philosophy in Computer Sciences

    The University of Texas at Austin

  • 2007

    Bachelor of Science in Computer Sciences

    The University of Arkansas at Fayetteville

  • 2007

    Bachelor of Science in Mathematics

    The University of Arkansas at Fayetteville
    with Honors

  • 2002

    High School

    Lake Hamilton High School

Recent Experiences

University of Texas
June 2015 - Present
Postdoctoral Fellow
Developing an ACL2-based satisfiability solver.
University of Texas
2010 - 2015
Graduate Research Assistant
Mechanical verification of graph algorithms, satisfiability solvers, and satisfiability proof checkers. Development of new unsatisfiability proof formats.
University of Texas
2008 - 2015
Teaching Assistant
Four semesters of graduate and undergraduate courses with two additional semesters as grader

Contact

Email
firstname dot lastname at gmail dot com

Skills

ACL2
C
Java
C++
Beginner
Proficient
Expert

Publications

  • Efficient, Mechanically-Verified Validation of Satisfiability Solvers
    Nathan David Wetzler
    PhD dissertation, The University of Texas at Austin, May 2015.
    UT Digital Repository - preprint
  • Expressing symmetry breaking in DRAT proofs
    Marijn J. H. Heule, Warren A. Hunt, Jr., and Nathan Wetzler
    International Conference on Automated Deduction (CADE), 2015. To appear.
    Springer Link - preprint
  • Bridging the gap between easy generation and efficient verification of unsatisfiability proofs
    Marijn J. H. Heule, Warren A. Hunt, Jr., and Nathan Wetzler
    Software Testing, Verification, and Reliability (STVR), 24(8):593–607, 2014.
    Wiley Online Library - preprint
  • DRAT-trim: Efficient checking and trimming using expressive clausal proofs
    Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt, Jr.
    Theory and Applications of Satisfiability Testing (SAT), volume 8561 of LNCS, pages 422–429. Springer, 2014.
    Springer Link - preprint
  • Trimming while checking clausal proofs
    Marijn J. H. Heule, Warren A. Hunt, Jr., and Nathan Wetzler
    Formal Methods in Computer-Aided Design (FMCAD), pages 181–188. IEEE, 2013.
    IEEE Xplore Digital Library - preprint
  • Mechanical verification of SAT refutations with extended resolution
    Nathan Wetzler, Marijn J. H. Heule, and Warren A. Hunt, Jr.
    Interactive Theorem Proving (ITP), volume 7998 of LNCS, pages 229–244. Springer, 2013.
    Springer Link - preprint
  • Verifying refutations with extended resolution
    Marijn J. H. Heule, Warren A. Hunt, Jr., and Nathan Wetzler
    International Conference on Automated Deduction (CADE), volume 7898 of LNAI, pages 345–359. Springer, 2013.
    Springer Link - preprint
  • Partial words and the critical factorization theorem revisited
    Francine Blanchet-Sadri and Nathan D. Wetzler
    Theoretical Computer Science, 385(1):179–192, 2007.
    ScienceDirect

Projects/Software

Coming soon...