Keijo Heljanko

Professor (Associate Professor)

Research outputs

  1. 2011
  2. Published

    Model-based safety evaluation of automation systems (MODSAFE): MODSAFE summary report

    Valkonen, J., Björkman, K., Lahtinen, J., Ranta, J., Frits, J., Heljanko, K. & Niemelä, I., 2011, SAFIR2010, The Finnish Research Programme on Nuclear Power Plant Safety 2007-2010. Final Report. 2571 ed. p. 55-65 11 p. (VTT Tiedotteita - Valtion Teknillinen Tutkimuskeskus; no. 2571).

    Research output: Chapter in Book/Report/Conference proceedingChapterScientificpeer-review

  3. Published

    Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation

    Barnat, J. & Heljanko, K., 2011, Snowbird, Utah, USA. (Electronic Proceedings in Theoretical Computer Science)

    Research output: Book/ReportAnthologyScientificpeer-review

  4. 2010
  5. Published

    Efficient Model Checking of PSL Safety Properties

    Launiainen, T., Heljanko, K. & Junttila, T., 2010, The 10th International Conference on Application of Concurrency to System Design (ACSD'2010). Braga, p. 95-104

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  6. Published

    Experimental Comparison of Concolic and Random Testing for Java Card Applets

    Kähkönen, K., Kindermann, R., Heljanko, K. & Niemelä, I., 2010, Model Checking Software: 17th International SPIN Workshop, Enschede, The Netherlands, September 27-29, 2010. Proceedings. van de Pol, J. & Weber, M. (eds.). p. 22-39 (Lecture Notes in Computer Science; vol. 6349).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  7. 2009
  8. Published

    Formal Verification of Safety Automation Logic Designs

    Valkonen, J., Koskimies, M., Björkman, K., Heljanko, K., Niemelä, I. & Hämäläinen, J. J., 2009, Automaatio XVIII 2009 Seminaari.

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  9. Published

    Interface Specification Methods for Software Components

    Lampinen, J., Liedes, S., Kähkönen, K., Kauttio, J. & Heljanko, K., 2009, Espoo, p. 52, (TKK reports in information and computer science; no. TKK-ICS-R25).

    Research output: Working paperProfessional

  10. Published

    Model-Based Analysis of a Stepwise Shutdown Logic: MODSAFE 2008 Work Report

    Björkman, K., Frits, J., Valkonen, J., Heljanko, K. & Niemelä, I., 2009, Espoo, 36 p. (VTT Working Papers; no. 115).

    Research output: Working paperProfessional

  11. Published

    Tarmo: A framework for Parallelized Bounded Model Checking

    Wieringa, S., Niemenmaa, M. & Heljanko, K., 2009, The 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC'09). Brim, L. & Pol, J. V. D. (eds.). p. 62-76

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  12. Published

    The LIME Interface Specification Language and Runtime Monitoring Tool

    Kähkönen, K., Lampinen, J., Heljanko, K. & Niemelä, I., 2009, Runtime Verification : 9th International Workshop, RV 2009, Grenoble, France, June 26-28, 2009. Selected Papers. Bensalem, S. & Peled, D. (eds.). p. 93-100 (Lecture Notes in Computer Science ; vol. 5779).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  13. Published

    Verification of Safety Logic Designs by Model Checking

    Björkman, K., Frits, J., Valkonen, J., Lahtinen, J., Heljanko, K., Niemelä, I. & Hämäläinen, J. J., 2009, 6th American Nuclear Society International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies NPIC&HMIT 2009. Knoxville, p. 324-335

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  14. 2008
  15. Published

    Analyzing Context-Free Grammars Using an Incremental SAT Solver

    Axelsson, R., Heljanko, K. & Lange, M., 2008, The 35th International Colloquium on Automata, Languages, and Programming (ICALP'08), Part II. Aceto, L., Damgård, I., Goldberg, L. A., Halldórsson, M. M., Ingólfsdóttir, A. & Walukiewicz, I. (eds.). Reykjavik, p. 410-422

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  16. Published

    Formal Verification of Safety I&C System Designs: Two Nuclear Power Plant Related Applications

    Valkonen, J., Koskimies, M., Pettersson, V., Heljanko, K., Holmberg, J-E., Niemelä, I. & Hämäläinen, J. J., 2008, Enlarged Halden Programme Group Meeting - Proceedings of the Man-Technology-Organisation Sessions, Institutt for Energiteknikk, Halden, Norway, 2008. Loen, p. C4.2

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientific

  17. Published

    Model-Based Analysis of an Arc Protection and an Emergency Cooling System: MODSAFE 2007 Work Report

    Valkonen, J., Petterson, V., Björkman, K., Holmberg, J-E., Koskimies, M., Heljanko, K. & Niemelä, I., 2008, Espoo: VTT, (VTT Working Papers; no. VTT-WP-93).

    Research output: Working paperProfessional

  18. Published

    NPP Safety Automation Systems Analysis: State of the Art

    Valkonen, J., Karanta, I., Koskimies, M., Heljanko, K., Niemelä, I., Sheridan, D. & Bloomfield, R. E., 2008, Espoo: VTT, 62 p. (VTT Working Papers; no. VTT-WP-94).

    Research output: Working paperProfessional

  19. Published

    Symbolic Step Encodings for Object Based Communicating State Machines

    Dubrovin, J., Junttila, T. & Heljanko, K., 2008, Formal Methods for Open Object-based Distributed Systems (FMOODS'08). Barthe, G. & de Boer, F. S. (eds.). Oslo, Norway, p. 96-112

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  20. Published

    Unfoldings - A Partial Order Approach to Model Checking

    Esparza, J. & Heljanko, K., 2008, Berlin. 172 p.

    Research output: Book/ReportBookScientificpeer-review

  21. 2007
  22. Published

    Symbolic Step Encodings for Object Based Communicating State Machines

    Dubrovin, J., Junttila, T. & Heljanko, K., 2007, Espoo, (Helsinki University of Technology Laboratory for Theoretical Computer Science Technical Reports; no. B24).

    Research output: Working paperProfessional

  23. 2006
  24. Published

    Bounded Model Checking for Weak Alternating Buchi Automata

    Heljanko, K., Junttila, T., Keinänen, M., Lange, M. & Latvala, T., 2006, Computer Aided Verification 2006, Seattle, WA, USA, 17.-20.8.2006. Ball, T. & Jones, R. B. (eds.). p. 95-108

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  25. Published

    Linear Encodings of Bounded LTL Model Checking

    Biere, A., Heljanko, K., Junttila, T., Latvala, T. & Schuppan, V., 2006, In : LOGICAL METHODS IN COMPUTER SCIENCE. 2, 5:5, p. 1-64

    Research output: Contribution to journalArticleScientificpeer-review

  26. Published

    Planning as satisfiability: Parallel plans and algorithms for plan search

    Rintanen, J., Heljanko, K. & Niemelä, I., 2006, In : Artificial Intelligence. 170, 12-13, p. 1031-1080

    Research output: Contribution to journalArticleScientificpeer-review

  27. 2005
  28. Published

    BMC via on-the-fly Determinization

    Jussila, T., Heljanko, K. & Niemelä, I., 2005, In : International Journal on Software Tools for Technology Transfer. 7, 2, p. 89-101 13 p.

    Research output: Contribution to journalArticleScientificpeer-review

  29. Published

    Complexity Results for Checking Distributed Implementability

    Heljanko, K. & Stefanescu, A., 2005, Application of Concurrency to System Design (ACSD'2005), St Malo, France, June 7-9, 2005. Desel, J. & Watanabe, Y. (eds.). Los Alamos, Clifornia, USA: IEEE Computer Society, p. 78-87

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  30. Published

    Incremental and Complete Bounded Model Checking for Full PLTL

    Heljanko, K., Junttila, T. & Latvala, TI., 2005, Computer Aided Verification 2005, Edinburgh,UK, 6-10.7.2005. Etessami, K. & Rajamani, S. K. (eds.). p. 98-111

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  31. Published

    Simple is Better: Efficient Bounded Model Checking for Past LTL

    Latvala, T., Biere, A., Heljanko, K. & Junttila, T., 2005, Verification, Model Checking, and Abstract Interpretation, Paris, France, 17-19 January 2005. Radhia, C. (ed.). Berlin, p. 380-395

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  32. 2004
  33. Published

    Complexity Results for Checking Distributed Implementability

    Heljanko, K. & Stefanescu, A., 2004, Stuttgart, Saksa, (Technical Report; no. 05/2004).

    Research output: Working paperProfessional

  34. Published

    Parallel encodings of classical planning as satisfiability

    Rintanen, J., Heljanko, K. & Niemelä, I., 2004, Freiburg, Germany, (Technical Reports; no. 198).

    Research output: Working paperProfessional

  35. Published

    Parallel Encodings of Classical Planning as Satisfiability

    Rintanen, J., Niemelä, I. & Heljanko, K., 2004, Logics in Artificial Intelligence : 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27-30, 2004. Proceedings. Alferes, J. J. & Leite, J. (eds.). Berlin, Germany, p. 307-319 (Lecture Notes in Computer Science ; vol. 3229).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  36. Published

    Planning as Satisfiability: Parallel Plans and Algorithms for Plan Search

    Rintanen, J., Heljanko, K. & Niemelä, I., 2004, Freiburg, Germany: Albert-Ludwigs-Universität Freiburg, 56 p. (Technical Reports of the Institute of Computer Science at Freiburg University; no. 216).

    Research output: Working paperProfessional

  37. Published

    PROD 3.4.00 -saavutettavuusanalyysiohjelmisto

    Anderson, L., Helander, J., Heljanko, K., Janhunen, T., Jürgens, R., Kangas, I., Nurmela, K., Oksanen, K., Pesonen, O., Rauhamaa, M. & 5 othersReilly, J., Suonsivu, H., Valkealahti, K., Varpaaniemi, K. & Väisänen, P., 2004

    Research output: Artistic and non-textual formSoftwareScientific

  38. Published

    Simple bounded LTL model checking

    Latvala, T., Biere, A., Heljanko, K. & Junttila, T., 2004, Espoo, (Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports; no. HUT-TCS-A92).

    Research output: Working paperProfessional

  39. Published

    Simple Bounded LTL Model Checking

    Latvala, T., Biere, A., Heljanko, K. & Junttila, T., 2004, Formal Methods in Computer-Aided Design 2004, Austin, Texas, USA, 15.-17.11.2004. Hu, A. J. & Martin, A. K. (eds.). Berliini, Saksa, p. 186-200

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  40. 2003
  41. Published

    BMC via on-the-fly Determinization

    Jussila, T., Heljanko, K. & Niemelä, I., 2003, In : ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. 89, 4, p. 561-577 17 p.

    Research output: Contribution to journalArticleScientificpeer-review

  42. Published

    Bomotest - A formal conformance testing tool, Version 1.5

    Pyhälä, T. & Heljanko, K., 2003

    Research output: Artistic and non-textual formSoftwareScientific

  43. Published

    Bounded LTL Model Checking with Stable Models

    Heljanko, K. & Niemelä, I., 2003, In : Theory and Practice of Logic Programming. 3, 4 & 5, p. 519-550

    Research output: Contribution to journalArticleScientificpeer-review

  44. Published

    Specification Coverage Aided Test Selection

    Pyhälä, T. & Heljanko, K., 2003, 3rd International Conference on Application of Concurrency to System Design (ACSD'2003), Guimaraes, Portugal, 18-20 June 2003. Balarin, F., Lilius, J. & Machado, R. J. (eds.). Guimaraes, Portugal: IEEE Computer Society, p. 187-195

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  45. 2002
  46. Published

    Parallelisation of the Petri Net Unfolding Algorithm.

    Heljanko, K., Khomenko, V. & Koutny, M., 2002, The 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2002), Grenoble, France, April 2002. Katoen, J-P. & Stevens, P. (eds.). Berlin, Germany, p. 371-385

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  47. Published

    Testing LTL Formula Translation into Büchi Automata

    Tauriainen, H. & Heljanko, K., 2002, In : International Journal on Software Tools for Technology Transfer. 4, 1, p. 57-70

    Research output: Contribution to journalArticleScientificpeer-review

  48. 2001
  49. Published

    Answer Set Programming and Bounded Model Checking

    Heljanko, K. & Niemelä, I., 2001, AAAI Spring 2001 Symposium on Answer Set Programming, Stanford CA, USA, 26.-28.3.2001: Towards Efficient and Scalable Knowledge Representation and Reasoning. Menlo Park CA, USA, p. 90-96

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  50. Published

    Bounded LTL Model Checking with Stable Models

    Heljanko, K. & Niemelä, I., 2001, 6th International Conference on Logic Programming and Nonmonotonic Reasoning, Vienna, Austria, September 17-19, 2001. Eiter, T., Faber, W. & Truszczynski, M. (eds.). Berlin, p. 200-212

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  51. Published

    Bounded Reachability Checking with Process Semantics

    Heljanko, K., 2001, 12th International Conference on Concurrency Theory (Concur'2001), Aalborg, Denmark, August 21-24, 2001. Larsen, K. G. & Nielsen, M. (eds.). Berlin, Germany, p. 218-232

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  52. Published

    boundsmodels 0.9: a bounded LTL model checker

    Heljanko, K. & Simons, P., 2001

    Research output: Artistic and non-textual formSoftwareScientific

  53. Published

    Implementing LTL Model Checking with Net Unfoldings

    Esparza, J. & Heljanko, K., 2001, 8th International SPIN Workshop on Model Checking of Software, Toronto, Canada, May 19-20, 2001. Dwyer, M. B. (ed.). Berlin, p. 37-56

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  54. Published

    Implementing LTL Model Checking with Net Unfoldings

    Esparza, J. & Heljanko, K., 2001, Espoo, p. 29, (Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports; no. HUT-TCS-A68).

    Research output: Working paperProfessional

  55. Published

    Parallelisation of the Petri Net Unfolding Algorithm

    Heljanko, K., Khomenko, V. & Koutny, M., 2001, Newcastle upon Tyne, UK, p. 14, (Department of Computing Science, University of Newcastle upon Tyne, Technical Reports; no. CS-TR-733).

    Research output: Working paperProfessional

  56. Published

    PROD 3.3.09 -saavutettavuusanalyysiohjelmisto

    Anderson, L., Helander, J., Heljanko, K., Janhunen, T., Jürgens, R., Kangas, I., Nurmela, K., Oksanen, K., Pesonen, O., Rauhamaa, M. & 5 othersReilly, J., Suonsivu, H., Valkealahti, K., Varpaaniemi, K. & Väisänen, P., 2001

    Research output: Artistic and non-textual formSoftwareScientific

  57. Published

    punroll 0.3: a bounded reachability checker

    Heljanko, K., 2001

    Research output: Artistic and non-textual formSoftwareScientific

  58. Published

    unfsmodels 0.9: an LTL model checker using net unfoldings

    Heljanko, K. & Simons, P., 2001

    Research output: Artistic and non-textual formSoftwareScientific

  59. 2000
  60. Published

    A New Unfolding Approach to LTL Model Checking

    Esparza, J. & Heljanko, K., 2000, The 27th International Colloquium on Automata, Languages and Programming, ICALP 2000, Geneva, Switzerland, July 2000. Montanari, U., Rolim, D. & Welzl, E. (eds.). Berlin, Germany, p. 475-486

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

  61. Published

    A New Unfolding Approach to LTL Model Checking

    Esparza, J. & Heljanko, K., 2000, Espoo, p. 32, (Helsinki University of Technology, Laboratory for Theoretical Computer Science, Research Reports; no. HUT-TCS-A60).

    Research output: Working paperProfessional

  62. Published

    Coping with Strong Fairness

    Latvala, T. & Heljanko, K., 2000, In : Fundamenta Informaticae. 43, 1-4, p. 175-193

    Research output: Contribution to journalArticleScientificpeer-review

ID: 66590