|
Timo Latvala |
| Researcher, D.Sc. (Tech.) |
I have moved to the Department of Computer
Science at the University of Illinois at Urbana-Champaign. I am still updating this page.
| 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 |
| Email: |
forename.surename tkk.fi |
Research Interests |
|
Model checking, SAT-based model checking, runtime verification, abstraction, complexity, Petri nets, ...
|
Teaching |
|
Spring 2005 I will lecture Introduction to Theoretical
Computer Science.
|
| |
|
| |
Software |
- 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...
|
|
