Publications

Books

• Esparza, J. and Heljanko, K.: Unfoldings - A Partial-Order Approach to Model Checking. EATCS Monographs in Theoretical Computer Science, Springer, ISBN 978-3-540-77425-9, 172 p., 2008. Book Flyer. Author created final book draft made available through our publishing agreement with Springer. It can not be made available on any other Web sites than the author homepages.

Refereed Journal Articles

• Lahtinen, J., Valkonen, J., Björkman, K., Frits, J., Niemelä, I., and Heljanko, K.: Model Checking of Safety-Critical Software in the Nuclear Engineering Domain. Reliability Engineering & System Safety (RESS), to appear. (doi: 10.1016/j.ress.2012.03.021).
• Niemenmaa, M., Kallio, A., Schumacher, A., Klemelä, P., Korpelainen, E., and Heljanko, K.: Hadoop-BAM: Directly Manipulating Next Generation Sequencing Data in the Cloud. Bioinformatics 28(6):876-877, 2012. (doi: 10.1093/bioinformatics/bts054).
• Heljanko, K., Keinänen, M., Lange, M., and Niemelä, I.: Solving Parity Games by a Reduction to SAT. Journal of Computer and System Sciences 78(2):430-440, 2012. (doi: 10.1016/j.jcss.2011.05.004).
• Launiainen, T., Heljanko, K., and Junttila, T.: Efficient Model Checking of PSL Safety Properties. IET Computers & Digital Techniques 5(6):479-492, 2011. (doi: 10.1049/iet-cdt.2010.0154).
• Dubrovin, J., Junttila, T., and Heljanko, K.: Exploiting Step Semantics for Efficient Bounded Model Checking of Asynchronous Systems. Science of Computer Programming, article in press. (doi: 10.1016/j.scico.2011.07.005).
• Biere, A., Heljanko, K., Junttila, T., Latvala, T., and Schuppan, V.: Linear Encodings of Bounded LTL Model Checking. Logical Methods in Computer Science 2(5:5):1-64, 2006. (An Open Access Journal listed in ISI Web of Knowledge, doi: 10.2168/LMCS-2(5:5)2006).
• Rintanen, J., Heljanko, K., and Niemelä, I.: Planning as Satisfiability: Parallel Plans and Algorithms for Plan Search. Artificial Intelligence 170(12-13):1031-1080, © Elsevier (publisher version), 2006.
• Jussila, T., Heljanko, K., and Niemelä, I.: BMC via On-the-Fly Determinization. STTT - International Journal on Software Tools for Technology Transfer, 7(2):89-101, © Springer (publisher version), 2005.
• Heljanko, K. and Niemelä, I.: Bounded LTL Model Checking with Stable Models. (CoRR: arXiv:cs.LO/0305040). Theory and Practice of Logic Programming (TPLP), 3(4&5):519-550, © Cambridge University Press, 2003 (see also experiments).
• Tauriainen, H. and Heljanko, K.: Testing LTL Formula Translation into Büchi Automata. STTT - International Journal on Software Tools for Technology Transfer, 4(1):57-70, 2002, © Springer (publisher version).
• Latvala, T. and Heljanko, K.: Coping with Strong Fairness. Fundamenta Informaticae, 43(1-4):175-193, IOS Press, 2000.
• Heljanko, K.: Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets. Fundamenta Informaticae, 37(3):247-268, IOS Press, 1999.

Refereed Conferences and Workshops

• Saarikivi, O., Kähkönen, K., and Heljanko,K.: Improving Dynamic Partial Order Reductions for Concolic Testing. In Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD 2012), to appear.
• Gan, X., Dubrovin, J. and Heljanko, K.: A Symbolic Model Checking Approach to Verifying Satellite Onboard Software. In Proceedings of the 11th International Workshop on Automated Verification of Critical Systems (AVoCS 2011), Newcastle, UK, September 2011.
• Kähkönen, K., Launiainen, T, Saarikivi, O., Kauttio, J., Heljanko, K., and Niemelä, I.: LCT: An Open Source Concolic Testing Tool for Java Programs. In Proceedings of the 6th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'2011), pages 75-80, Saarbrucken, Germany, Mar 2011.
• Kähkönen, K., Kindermann, R., Heljanko, K., and Niemelä, I.: Experimental Comparison of Concolic and Random Testing for Java Card Applets. In Proceedings of the 17th International SPIN Workshop on Model Checking of Software (SPIN'2010), pages 22-39, Lecture Notes in Computer Science 6349, Twente, The Netherlands, September 2010, © Springer (publisher version).
• Launiainen, T., Heljanko, K., Junttila, T.: Efficient Model Checking of PSL Safety Properties, In Proceedings of the 10th International Conference on Application of Concurrency to System Design (ACSD'2010), pages 95-104, IEEE Computer Society Press, Braga, Portugal, June 2010.
• Wieringa, S., Niemenmaa, M., Heljanko, K.: Tarmo: A Framework for Parallelized Bounded Model Checking, In Proceedings of the 8th International Workshop on Parallel and Distributed Methods in Verification (PDMC'09), Electronic Proceedings in Theoretical Computer Science (EPTCS) 14, pages 62-76, 2009.
• Kähkönen, K., Lampinen, J., Heljanko, K., and Niemelä, I.: The LIME Interface Specification Language and Runtime Monitoring Tool. In Proceedings of the 9th International Workshop on Runtime Verification, pages 93-100, Lecture Note in Computer Science 5779, Grenoble, France, June 2009, © Springer (publisher version).
• Axelsson, R., Heljanko, K., and Lange, M.: Analyzing Context-Free Grammars Using an Incremental SAT Solver. In Proceedings of the 35th International Colloquium on Automata, Languages, and Programming (ICALP'08), Part II, pages 410-422, Lecture Notes in Computer Science 5126, Reykjavik, Iceland, July 2008, © Springer (publisher version).
• Dubrovin, J., Junttila, T., and Heljanko, K.: Symbolic Step Encodings for Object Based Communicating State Machines. In Proceedings of the 10th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), pages 96-112, Lecture Notes in Computer Science 5051, Oslo, Norway, June 2008, © Springer (publisher version).
• Heljanko, K., Junttila, T., Keinänen, M., Lange, M., and Latvala, T.: Bounded Model Checking for Weak Alternating Buchi Automata. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV'2006), pages 95-108, Lecture Notes in Computer Science 4144, Seattle, WA, USA, August 2006. © Springer (publisher version).
• Heljanko, K., Junttila, T., and Latvala, T.: Incremental and Complete Bounded Model Checking for Full PLTL. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV'2005), pages 98-111, Lecture Notes in Computer Science 3576, Edinburgh, Scotland, United Kingdom, July 2005. © Springer (publisher version).
• Heljanko, K. and Ştefănescu, A.: Complexity Results for Checking Distributed Implementability. In Proceedings of the 5th International Conference on Application of Concurrency to System Design (ACSD'2005), pages 78-87, St Malo, France, June 2005. © IEEE Computer Society Press.
• Latvala, T., Biere, A., Heljanko, K., and Junttila, T.: Simple Is Better: Efficient Bounded Model Checking for Past LTL. In Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'2005), pages 380-395, Lecture Notes in Computer Science 3385, Paris, France, January 2005. © Springer (publisher version).
• Latvala, T., Biere, A., Heljanko, K., and Junttila, T.: Simple Bounded LTL Model Checking. In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'2004), pages 186-200, Lecture Notes in Computer Science 3312, Austin, Texas, USA, November 2004. © Springer (publisher version).
• Rintanen, J., Heljanko, K., and Niemelä, I.: Parallel Encodings of Classical Planning as Satisfiability. In Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA'2004), pages 307-319, Lecture Notes in Computer Science 3229, Lisbon, Portugal, September 2004. © Springer.
• Jussila, T., Heljanko, K., and Niemelä, I.: BMC via On-the-Fly Determinization. In Proceedings of the First International Workshop on Bounded Model Checking (BMC'2003), Electronic Notes in Theoretical Computer Science 89(4):561-577, Boulder, Colorado, USA, July 2003. © Elsevier.
• Pyhälä, T. and Heljanko, K.: Specification Coverage Aided Test Selection. In Proceedings of the 3rd International Conference on Application of Concurrency to System Design (ACSD'2003), pages 187-195, Guimaraes, Portugal, June 2003. © IEEE Computer Society.
• Heljanko, K., Khomenko, V., and Koutny, M.: Parallelisation of the Petri Net Unfolding Algorithm. In Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2002), pages 371-385, Lecture Notes in Computer Science 2280, Grenoble, France, April 2002. © Springer (publisher version).
• Heljanko, K. and Niemelä, I.: Bounded LTL Model Checking with Stable Models. In Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'2001), pages 200-212, Lecture Notes in Artificial Intelligence 2173, Vienna, Austria, September 2001. © Springer (see also experiments).
• Heljanko, K.: Bounded Reachability Checking with Process Semantics. In Proceedings of the 12th International Conference on Concurrency Theory (Concur'2001), pages 218-232, Lecture Notes in Computer Science 2154, Aalborg, Denmark, August 2001. © Springer (publisher version, see also experiments).
• Esparza, J. and Heljanko, K.: Implementing LTL Model Checking with Net Unfoldings. In Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN'2001), pages 37-56, Lecture Notes in Computer Science 2057, Toronto, Canada, May 2001. © Springer (publisher version, see also experiments).
• Heljanko, K. and Niemelä, I.: Answer Set Programming and Bounded Model Checking. In Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning, AAAI Press, Technical Report SS-01-01, pages 90-96, Stanford, USA, March 2001 (see also experiments).
• Tauriainen, H. and Heljanko, K.: Testing SPIN's LTL Formula Conversion into Büchi Automata with Randomly Generated Input. In Proceedings of the 7th International SPIN Workshop on Model Checking of Software (SPIN'2000), pages 54-72, Lecture Notes in Computer Science 1885, Stanford University, California, USA, August 2000. © Springer.
• Heljanko, K.: Model Checking with Finite Complete Prefixes is PSPACE-complete. In Proceedings of the 11th International Conference on Concurrency Theory (Concur'2000), pages 108-122, Lecture Notes in Computer Science 1877, State College, Pennsylvania, USA, August 2000. © Springer (publisher version).
• Esparza, J. and Heljanko, K.: A New Unfolding Approach to LTL Model Checking. In Proceedings of the 27th International Colloquium on Automata, Languages and Programming (ICALP'2000), pages 475-486, Lecture Notes in Computer Science 1853, Geneva, Switzerland, July 2000. © Springer (publisher version).
• Latvala, T. and Heljanko, K.: Coping with Strong Fairness - On-the-fly Emptiness Checking for Streett Automata. In Proceedings of the Workshop Concurrency, Specification & Programming 1999 (CS&P' 99), pages 107-118, Warsaw, Poland, September 1999. Full version.
• Heljanko, K.: Minimizing Finite Complete Prefixes. In Proceedings of the Workshop Concurrency, Specification & Programming 1999 (CS&P' 99), pages 83-95, Warsaw, Poland, September 1999. Full version.
• Heljanko, K.: Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets. In Proceedings of the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), pages 240-254, Lecture Notes in Computer Science 1579, Springer, Berlin, March 1999. © Springer. (See also experiments).
• Heljanko, K.: Deadlock Checking for Complete Finite Prefixes Using Logic Programs with Stable Model Semantics (Extended Abstract). In Proceedings of the Workshop Concurrency, Specification & Programming 1998 (CS&P' 98), pages 106-115, Informatik-Bericht Nr. 110, Humboldt-University, Berlin, September 1998.
• Varpaaniemi, K., Heljanko, K., Lilius, J.: PROD 3.2 - An Advanced Tool for Efficient Reachability Analysis. In Grumberg, O. (ed.): Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97), pages 472-475, Lecture Notes in Computer Science 1254, Springer, Berlin, June 1997.
• Heljanko, K.: Implementing a CTL Model Checker. In Proceedings of the Workshop Concurrency, Specification & Programming 1996 (CS&P' 96), Informatik-Bericht Nr. 69, pages 75-84, Humboldt-University, Berlin, September 1996.

  Theses

• Heljanko, K.: Combining Symbolic and Partial Order Methods for Model Checking 1-Safe Petri Nets. D.Sc.(Tech.) Thesis, 2002.
• Heljanko, K.: Deadlock and Reachability Checking with Finite Complete Prefixes. Research Report A56, Laboratory for Theoretical Computer Science, Helsinki University of Technology, Espoo, Finland, December 1999, 70p (see also experiments). Licentiate's Thesis.
• Heljanko, K.: Model Checking the Branching Time Temporal Logic CTL. Research Report A45, Digital Systems Laboratory, Helsinki University of Technology, Espoo, May 1997, 71 p. Master's Thesis.

  Technical Reports and Other Non-Refereed Scientific Publications

• Lahtinen, J., Launiainen, T., Heljanko, K., and Ropponen, J.: Model Checking Methodology for Large Systems, Faults and Asynchronous Behaviour - SARANA 2011 Work Report. VTT Technology 12, VTT Technical Research Centre of Finland, Espoo, 2012.
• Lampinen, J., Liedes, S., Kähkönen, K., Kauttio, J., and Heljanko, K. Interface specification methods for software components. Technical Report TKK-ICS-R25, Helsinki University of Technology, Department of Information and Computer Science, Espoo, Finland, December 2009.
• Björkman, K., Frits, J., Valkonen, J., Lahtinen, J., Heljanko, K., Niemelä, I., and Hämäläinen, J. J.: Verification of Safety Logic Designs by Model Checking Sixth American Nuclear Society International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies (NPIC&HMIT 2009), Knoxville, Tennessee, April 5-9, 12 p., on CD-ROM, American Nuclear Society, LaGrande Park, IL, 2009.
• Valkonen, J., Koskimies, M., Björkman, K., Heljanko, K., Niemelä, I., and Hämäläinen, J. J.: Formal Verification of Safety Automation Logic Designs Automaatio XVIII Seminaari 2009, 17-18.3.2009, Helsinki, Suomen Automaatioseura, 2009.
• Björkman, K., Frits, J., Valkonen, J., Heljanko, K., and Niemelä, I.: Model-Based Analysis of a Stepwise Shutdown Logic - MODSAFE 2008 Work Report. VTT Working Papers 115, VTT Technical Research Centre of Finland, Espoo, Finland, Mar 2009, 41 p.
• Valkonen, J., Koskimies, M., Pettersson, V., Heljanko, K., Holmberg, J.-E., Niemelä, I., and Hämäläinen, J. J.: Formal verification of safety I&C system designs: Two nuclear power plant related applications. In Enlarged Halden Programme Group Meeting - Proceedings of the Man-Technology-Organisation Sessions, page C4.2. Institutt for Energiteknikk, Halden, Norway, May 2008.
• Valkonen, J., Karanta, I., Koskimies, M., Heljanko, K., Niemelä, I., Sheridan, D., and Bloomfield, R. E.: NPP Safety Automation Systems Analysis - State of the Art. VTT Working Papers 94, VTT Technical Research Centre of Finland, Espoo, Finland, April 2008, 62 p.
• Valkonen, J., Petterson, V., Björkman, K., Holmberg, J.-E., Koskimies, M., Heljanko, K., and Niemelä, I.: Model-Based Analysis of an Arc Protection and an Emergency Cooling System - MODSAFE 2007 Working Report. VTT Working Papers 93, VTT Technical Research Centre of Finland, Espoo, Finland, February 2008, 51 p.
• Heljanko, K.: Verification Methods Based on Propositional Logic Satisfiability. Abstract in the Abstract collection of Finnish Mathematical Days 2008, Espoo, Finland, Jan 3-4, 1p.
• Dubrovin, J. and Junttila, T., and Heljanko, K.: Symbolic Step Encodings for Object Based Communicating State Machines. Technical Report B24, Laboratory for Theoretical Computer Science, Helsinki University of Technology, Espoo, Finland, December 2007, 25 p.
• Rintanen, J., Heljanko, K., and Niemelä, I.: Planning as Satisfiability: Parallel Plans and Algorithms for Plan Search. Technical report 216, Institute of Computer Science at Freiburg University, 2005, 56p.
• Heljanko, K. and Ştefănescu, A.: Complexity Results for Checking Distributed Implementability. Technical Report 05/2004, Institute of Formal Methods in Computer Science, University of Stuttgart, October 2004, 37p.
• Latvala, T., Biere, A., Heljanko, K., and Junttila, T.: Simple bounded LTL model checking. Research Report A92, Laboratory for Theoretical Computer Science, Helsinki University of Technology, Espoo, Finland, July 2004, 16p.
• Rintanen, J., Heljanko, K., and Niemelä, I.: Parallel Encodings of Classical Planning as Satisfiability. Technical report 198, Institute of Computer Science at Freiburg University, February 2004, 8p.
• Heljanko, K., Khomenko, V., and Koutny, M.: Parallelisation of the Petri Net Unfolding Algorithm. Technical Report CS-TR-733, Department of Computing Science, University of Newcastle upon Tyne, June 2001, 14p.
• Esparza, J. and Heljanko, K.: Implementing LTL Model Checking with Net Unfoldings. Research Report A68, Laboratory for Theoretical Computer Science, Helsinki University of Technology, Espoo, Finland, March 2001, 29p.
• Heljanko, K. and Niemelä, I.: Petri Net Analysis and Nonmonotonic Reasoning. In Leksa Notes in Computer Science, Festschrift in Honour of Professor Leo Ojala, pages 7-19. Helsinki University of Technology, Laboratory for Theoretical Computer Science, October 2000.
• Esparza, J. and Heljanko, K. A New Unfolding Approach to LTL Model Checking. Research Report A60, Laboratory for Theoretical Computer Science, Helsinki University of Technology, Espoo, Finland, April 2000, 32p.