College of Computer and Information Science

Northeastern University
360 Huntington Avenue
Boston, Massachusetts 02115

Office: 202 West Village H, room 344
wahl[ -- ät -- ]
                                      Thomas Wahl                   
Northeastern University


  • My student Peizun Liu's paper about executing an infinite-state backward reachability algorithm directly on Boolean programs has been accepted to FMCAD 2014
  • A joint paper with Alexander Kaiser and Daniel Kroening about the limits of predicate abstraction for unbounded-thread concurrent systems has been accepted to CONCUR 2014
  • Another joint paper with Alexander Kaiser and Daniel Kroening, this one about efficiently combining infinite-state forward and backward searches through Petri nets and the like has been accepted to TOPLAS, an ACM journal

Conference program or organizing committees:

Brief bio:

  • 2011 - present: Assistant Professor, Northeastern University, College of Computer and Information Science
  • 2009 - 2011: Research Assistant, Oxford University, Department of Computer Science (formerly "Computing Laboratory"), UK
  • 2007 - 2009: Lecturer and Postdoc, Swiss Federal Institute of Technology (ETH), Zurich, Switzerland
  • 2007, 2005: Ph.D. & M.S., University of Texas, Austin
  • 1998: Invited Researcher, Advanced Telecommunications Research (ATR), Nara, Japan
  • 1997: University Diploma in Informatics, Würzburg, Germany


General research interests:

  • Software verification, such as using predicate abstraction, SAT- and SMT solvers, decision procedures, interpolation;
  • Infinite-state system verification, such as modeling and analyzing arbitrarily replicated multi-threaded programs via counter systems and Petri nets;
  • Automata theory in formal verification, such as for LTL model checking

Research sponsors:

National Science
                                      Foundation Draper Labs
Page last modified in Fall 2014. Design borrowed in part from Domagoj Babic