Keijo Heljanko
Professor (Associate Professor)
Research outputs
- 2011
- Published
LCT: An Open Source Concolic Testing Tool for Java Programs
Kähkönen, K., Launiainen, T., Saarikivi, O., Kauttio, J., Heljanko, K. & Niemelä, I., 2011, 6th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'2011). Saarbrücken, p. 75-80Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 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 proceeding › Chapter › Scientific › peer-review
- 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/Report › Anthology
- 2010
- 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-104Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 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 proceeding › Conference contribution › Scientific › peer-review
- 2009
- 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 proceeding › Conference contribution › Scientific › peer-review
- 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 paper › Professional
- 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 paper › Professional
- 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-76Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 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 proceeding › Conference contribution › Scientific › peer-review
- 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-335Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 2008
- 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-422Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 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.2Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific
- 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 paper › Professional
- 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 paper › Professional
- 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-112Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- Published
Unfoldings - A Partial Order Approach to Model Checking
Esparza, J. & Heljanko, K., 2008, Berlin. 172 p.Research output: Book/Report › Book
- 2007
- 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 paper › Professional
- 2006
- 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-108Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 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-64Research output: Contribution to journal › Article › Scientific › peer-review
- 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-1080Research output: Contribution to journal › Article › Scientific › peer-review
- 2005
- 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 journal › Article › Scientific › peer-review
- 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-87Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 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-111Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 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-395Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 2004
- Published
Complexity Results for Checking Distributed Implementability
Heljanko, K. & Stefanescu, A., 2004, Stuttgart, Saksa, (Technical Report; no. 05/2004).Research output: Working paper › Professional
- Published
Parallel encodings of classical planning as satisfiability
Rintanen, J., Heljanko, K. & Niemelä, I., 2004, Freiburg, Germany, (Technical Reports; no. 198).Research output: Working paper › Professional
- 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 proceeding › Conference contribution › Scientific › peer-review
- 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 paper › Professional
- 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 others, , 2004Research output: Artistic and non-textual form › Software › Scientific
- 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 paper › Professional
- 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-200Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 2003
- 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 journal › Article › Scientific › peer-review
- Published
Bomotest - A formal conformance testing tool, Version 1.5
Pyhälä, T. & Heljanko, K., 2003Research output: Artistic and non-textual form › Software › Scientific
- 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-550Research output: Contribution to journal › Article › Scientific › peer-review
- 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-195Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 2002
- 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-385Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 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-70Research output: Contribution to journal › Article › Scientific › peer-review
- 2001
- 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-96Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 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-212Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 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-232Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- Published
boundsmodels 0.9: a bounded LTL model checker
Heljanko, K. & Simons, P., 2001Research output: Artistic and non-textual form › Software › Scientific
- 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-56Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 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 paper › Professional
- 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 paper › Professional
- 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 others, , 2001Research output: Artistic and non-textual form › Software › Scientific
- Published
punroll 0.3: a bounded reachability checker
Heljanko, K., 2001Research output: Artistic and non-textual form › Software › Scientific
- Published
unfsmodels 0.9: an LTL model checker using net unfoldings
Heljanko, K. & Simons, P., 2001Research output: Artistic and non-textual form › Software › Scientific
- 2000
- 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-486Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
- 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 paper › Professional
ID: 66590