TCS / Personnel / Timo Latvala
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science
I have moved to the Department of Computer Science at the University of Illinois at Urbana-Champaign. I am still updating this page.

Timo Latvala

Researcher, D.Sc. (Tech.)
Office: Room 2103, Thomas M. Siebel Center for Computer Science
Postal Address: 201 Goodwin Ave.
Urbana, IL 61801-2302
United States of America
Telephone: +1 217 244 4250

Research Interests

Model checking, SAT-based model checking, runtime verification, abstraction, complexity, Petri nets, ...


Spring 2005 I will lecture Introduction to Theoretical Computer Science.



  • I have implemented a new BMC encoding for PLTL in NuSMV. NuSMV-bPLTL extends the model checker NuSMV, version 2.1.2, with a new BMC encoding for PLTL. See our paper in VMCAI 2005 for details.
  • I have been involved in designing and implementing the model checking functionality for Maria.
  • scheck is a tool for translating LTL safety formulas to automata on finite words. The implementation is described in my SPIN 2003 paper.

Other Interests

  • Good books by authors such as Neil Gaiman, Terry Pratchet, Iain Banks,...
  • Sports, in particular football, floorball and golf.
  • Lots of other things...

[TCS main] [Contact Info] [Personnel] [Research] [Publications] [Software] [Studies] [News Archive] [Links]
Latest update: 05 October 2005.
Valid HTML 4.0! Valid CSS!