Publications

BibTeX Entries

Thesis

• Timo Latvala. Automata-Theoretic and Bounded Model Checking for Linear Temporal Logic. PhD Thesis. Technical Report A95, Laboratory for Theoretical Computer Science, Helsinki University Technology, Espoo, Finland, July 2005.
• Timo Latvala. On Model Checking Safety Properties. Licentiate's Thesis. Technical Report A76, Laboratory for Theoretical Computer Science, Helsinki University Technology, Espoo, Finland, Dec 2002.
• Timo Latvala. Model Checking Linear Temporal Logic Properties of Petri Nets with Fairness Constraints. Master's Thesis. Technical report A67, Laboratory for Theoretical Computer Science, Helsinki University of Technology, Espoo, Finland, Jan 2001.

Journal Papers

• T. Latvala and H. Tauriainen. Improved On-the-fly Verification with Testers. Nordic Journal of Computing, 11(2):148--164, 2004. pdf (117 kB). Copyright © Publishing Association Nordic Journal of Computing.
• T. Latvala and K. Heljanko. Coping with Strong Fairness. Fundamenta Informaticae, 43(1-4):175-193, 2000. Gzipped postscript(142 kB).

Conference and Workshop Papers

• K. Heljanko, T. Junttila and T. Latvala. Incremental and Complete Bounded Model Checking for Full PLTL. In K. Etessami and S. Rajamani (eds.), Computer Aided Verification, Edinburgh, Scotland, Volume 3576 of LNCS, pp. 98-111, Springer, 2005. PDF file (115 kB). Copyright © Springer-Verlag.
• T. Latvala, A. Biere, K. Heljanko, and T. Junttila. Simple is Better: Efficient Bounded Model Checking for Past LTL. In: R. Cousot (ed.), Verification, Model Checking, and Abstract Interpretation, 6th International Conference VMCAI 2005, Paris, France, Volume 3385 of LNCS, pp. 380-395, Springer, 2005. PDF file (154 kB), ps.gz file (185 kB). Copyright © Springer-Verlag. Slides for the presentation given at the conference.
• T. Latvala, A. Biere, K. Heljanko, and T. Junttila. Simple Bounded LTL Model Checking. In: Alan J. Hu and Andrew K. Martin (eds.), Formal Methods in Computer-Aided Design 2004, 5th International Conference FMCAD 2004, Austin, Texas, USA, Volume 3312 of LNCS, pp. 186-200, Springer, 2004. PDF file (203 kB). Copyright © Springer-Verlag. Slides for the presentation given at the conference. See also the tech report version of the paper.
• T. Latvala and Marko Mäkelä. LTL Model Checking for Modular Petri Nets. In: J. Cortadella and W. Reisig (eds.). Application and Theory of Petri Nets 2004. 25th International Conference, ICATPN 2004, Volume 3099 of LNCS, pp. 298-311, Springer, 2004. PDF file (274 kB). Copyright © Springer-Verlag. Slides for the presentation given at the conference.
• T. Latvala. Efficient Model Checking of Safety Properties. In: T. Ball and S.K. Rajamani (eds.), Model Checking Software. 10th International SPIN Workshop. Volume 2648 of LNCS, pp. 74-88, Springer, 2003. PDF file (270 kB). Copyright © Springer-Verlag. Slides for the presentation given at the conference.
• T. Latvala. Model Checking LTL properties of High-Level Petri Nets with Fairness Constraints. In: J-M Colom and Maciej Koutny (eds.), Application and Theory of Petri Nets 2001. 22nd International Conference (ICATPN'2001). Volume 2075 of LNCS, pp. 242-262, Newcastle upon Tyne, England, 2001. Slides for the presentation given at the conference. Gzipped postscript(130 kB). Copyright © Springer-Verlag.
• T. Latvala and K. Heljanko. Coping with Strong Fairness -- On-the-fly Emptiness Checking for Streett Automata. Proceedings of the CS & P'99 Workshop. H-D. Burkhard, L. Czaja, H-S. Nguyen and P. Starke (eds.), Warsaw, Poland, 1999. Full version, gzipped postscript (92 kB). Superseeded by the Fundamenta Informaticae paper "Coping with Strong Fairness".