Publications

• My Publications in the DBLP database
• My Publications in the Google Scholar citation index
• My ResearchGate profile
• My ResearcherID profile
• My ORCID profile
• My Scopus profile

• Some of the papers below available online are (late) draft versions due to copyright issues.

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.

Edited Proceedings

• Jeremy T. Bradley, Keijo Heljanko, William J. Knottenbelt, Nigel Thomas: Proceedings the Sixth International Workshop on the Practical Application of Stochastic Modelling (PASM) and the Eleventh International Workshop on Parallel and Distributed Methods in Verification (PDMC). Electr. Notes Theor. Comput. Sci. 296: (2013).
• Jens Brandt and Keijo Heljanko (eds.): Proceedings of the 12th International Conference on Application of Concurrency to System Design, ACSD 2012, Hamburg, Germany, June 27-29, 2012. IEEE 2012.
• Jiri Barnat and Keijo Heljanko (eds.): Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2011). EPTCS 72, 2011.

Refereed Journal Articles

• Maarala, A., Bzhalava, Z., Dillner, J., Heljanko, K., and Bzhalava, D.: ViraPipe: Scalable Parallel Pipeline for Viral Metagenome Analysis from Next Generation Sequencing Reads. Bioinformatics, btx702, 2017. Available online.
• Kähkönen, K. and Heljanko, K.: Testing Programs with Contextual Unfoldings. ACM Transactions on Embedded Computing Systems, 2017, accepted for publication.
• Saarikivi, O., Ponce-De-León, H., Kähkönen, K., Heljanko, K., and Esparza, J.: Minimizing test suites with unfoldings of multithreaded programs. ACM Transactions on Embedded Computing Systems, 16(2):45:1-45:24, 2017.
• Siirtola, A., Tripakis, S., and Heljanko, K.: When do we not need complex assume-guarantee rules? ACM Transactions on Embedded Computing Systems, 16(2):48:1-48:25, 2017.
• Dolev, D., Heljanko, K., Järvisalo, M., Korhonen, J.-H., Lenzen, C., Rybicki, J., Suomela, J., and Wieringa, S.: Synchronous counting and computational algorithm design. Journal of Computer and System Sciences, 82(2):310-332, 2016.
• Cabodi, G., Loiacono, C., Palena, M., Pasini, P., Patti, D., Quer, S., Vendraminetto, D., Biere, A., Heljanko, K.: Hardware Model Checking Competition 2014: An Analysis and Comparison of Model Checkers and Benchmarks. Journal on Satisfiability, Boolean Modeling and Computation, 9:135-172, 2015.
• Saarikivi, O. and Heljanko, K.: LCTD: Test-guided proofs for C programs on LLVM. Journal of Logical and Algebraic Methods in Programming, 2015. Article in press, available online.
• Siirtola, A. and Heljanko, K.: Parametrised modal interface automata. ACM Transactions on Embedded Computing Systems (TECS), 14(4):1-65, 2015. Article No. 65.
• Lahtinen, J., Kuismin, T., Heljanko, K.: Verifying large modular systems using iterative abstraction refinement. Reliability Engineering & System Safety, 139:120-130, 2015.
• Kähkönen, K., Saarikivi, O. and Heljanko, K.: Unfolding based automated testing of multithreaded programs. Automated Software Engineering, 22(4):475-515, 2015.
• Schumacher, A., Pireddu, L., Niemenmaa, M., Kallio, A., Korpelainen, E., Zanetti, G., and Heljanko, K.: SeqPig: Simple and scalable scripting for large sequencing data sets in Hadoop. Bioinformatics 30 (1): 119-120, 2014. (doi: 10.1093/bioinformatics/btt601).
• Gan, X., Dubrovin, J., and Heljanko, K.: A Symbolic Model Checking Approach to Verifying Satellite Onboard Software. Science of Computer Programming 82:44-55, 2014. (doi: 10.1016/j.scico.2013.03.005).
• 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) 105:104-113, 2012. (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).
• Dubrovin, J., Junttila, T., and Heljanko, K.: Exploiting Step Semantics for Efficient Bounded Model Checking of Asynchronous Systems. Science of Computer Programming 77(10-11):1095-1121, 2012. (doi: 10.1016/j.scico.2011.07.005).
• 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).
• 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 (doi: 10.1016/j.artint.2006.08.002), 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. (doi: 10.1017/S1471068403001790, 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 (doi: 10.1007/s100090200070).
• 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

• Hinkka, M., Lehto, T., Heljanko, K., and Jung, A.: Structural Feature Selection for Event Logs. In Proceedings of the Workshop on Business Process Innovation with Artificial Intelligence BPAI 2017, September 2017, Barcelona, Spain.
• Ponce-de-León, H., Furbach, F., Heljanko, K., and Meyer, R.: Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models. In Static Analysis - 24th International Symposium, SAS 2017, volume 10422 of Lecture Notes in Computer Science, pp. 299-320.
• Saarikivi, O., Heljanko, K.: LCTD: Tests-Guided Proofs for C Programs on LLVM - (Competition Contribution). In Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, volume 9636 of Lecture Notes in Computer Science, pp. 927-929.
• Hinkka, M., Lehto, T., and Heljanko, K.: Assessing Big Data SQL frameworks for analyzing event logs. In Proceedings of the 24th Euromicro International Conference on Parallel, Distributed and Network-Based Processing, Heraklion, Greece, pp. 101-108, 2016. IEEE.
• Ponce-de-León, H., Rodríguez, C., Carmona, J., Heljanko, K. and Haar, S.: Unfolding-based process discovery. In Proceedings of Automated Technology for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai, China, October 12-15, 2015, volume 9364 of Lecture Notes in Computer Science, pages 31-47. Springer, 2015.
• Saarikivi, O. and Heljanko, K.: Reporting Races in Dynamic Partial Order Reduction. In Proceedings of the 7th NASA Formal Methods Symposium (NFM 2015), Pasadena, California, USA, April 27-29, 2015, Lecture Notes in Computer Science 9058, 2015, pp. 450-456.
• Siirtola, A., Tripakis, S., and Heljanko, K.: When Do We (Not) Need Complex Assume-Guarantee Rules? In Proceedings of 15th International Conference on Application of Concurrency to System Design (ACSD 2015), pages 30-39, Brussels, Belgium, June 21st to 26th, 2015, IEEE Press.
• Ponce-de-León, H., Saarikivi, O., Kähkönen, K., and Heljanko, K.: Unfolding based Minimal Test Suites for Testing Multithreaded Programs. In Proceedings of 15th International Conference on Application of Concurrency to System Design (ACSD 2015), pages 40-49, Brussels, Belgium, June 21st to 26th, 2015, IEEE Press.
• Kähkönen, K. and Heljanko K.: Testing Multithreaded Programs with Contextual Unfoldings and Dynamic Symbolic Execution. In Proceedings of 14th International Conference on Application of Concurrency to System Design (ACSD 2014), pages 142-151, Tunis, Tunisia, June 23-27, 2014, IEEE Press.
• Kähkönen, K. and Heljanko, K.: Lightweight State Capturing for Automated Testing of Multithreaded Programs. In Tests and Proofs - 8th International Conference (TAP 2014), pages 187-203, Lecture Notes in Computer Science 8570, York, UK, July 24-25, 2014.
• Kuismin, T. and Heljanko, K.: Increasing Confidence in Liveness Model Checking Results with Proofs. In Proceedings of the 9th Haifa Verification Conference (HVC 2013), pages 32-43, Lecture Notes in Computer Science 8244, 2013, Haifa, Israel, 5-7 November 2013. (doi: 10.1007/978-3-319-03077-7_3).
• Wieringa, S. and Heljanko, K.: Concurrent Clause Strengthening. In Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), pages 116-132, Lecture Notes in Computer Science 7962, 2013, Helsinki, Finland, July 8-12, 2013. (doi: 10.1007/978-3-642-39071-5_10)
• Siirtola, A. and Heljanko, K.: Parametrised Compositional Verification with Multiple Process and Data Types. In Proceedings of the 13th International Conference on Application of Concurrency to System Design (ACSD 2013), pages 67-76, IEEE Computer Society, Barcelona, Spain, Jul 8-10, 2013. (doi: 10.1109/ACSD.2013.9)
• Wieringa, S. and Heljanko, K.: Asynchronous Multi-core Incremental SAT Solving. In Proceeding of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), pages 141-155, Lecture Notes in Computer Science 7795, 2013, (doi: 10.1007/978-3-642-36742-7_10).
• Kähkönen, K., Saarikivi, O., and Heljanko, K.: LCT: A Parallel Distributed Testing Tool for Multithreaded Java Programs. In Proceedings the Sixth International Workshop on the Practical Application of Stochastic Modelling (PASM'12) and the Eleventh International Workshop on Parallel and Distributed Methods in Verification (PDMC'12). Electronic Notes in Theoretical Computer Science (ENTCS), Volume 296, 16 August 2013, Pages 253-259. (doi: http://dx.doi.org/10.1016/j.entcs.2013.09.002).
• Kähkönen, K., Saarikivi, O., and Heljanko, K.: Using Unfoldings in Automated Testing of Multithreaded Programs. In Proceedings of the 27th IEEE/ACM International Conference Automated Software Engineering 2012 (ASE 2012), pages 150-159, Essen, Germany, September 2012. (doi: 10.1145/2351676.2351698).
• 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), pages 132-141, 25-29 June 2012, Hamburg, Germany. (doi: 10.1109/ACSD.2012.18).
• 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. Electronic Communications of the EASST 46, pages 1-15, 2012. (publisher version).
• 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 (doi: 10.1007/978-3-642-16164-3_3).
• 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 (doi: 10.1007/978-3-642-04694-0_7).
• 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 (doi: 10.1007/978-3-540-70583-3_34).
• 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 (doi: 10.1007/978-3-540-68863-1_7).
• 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 (doi: 10.1007/11817963_12).
• 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 (doi: 10.1007/11513988_10).
• 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

• Hinkka, M., Lehto, T., Heljanko, K., and Jung, A.: Structural Feature Selection for Event Logs, arXiv preprint, 2017.
• Ponce-De-León, H., Furbach, F., Heljanko, K., and Meyer., R.: Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all Models, arXiv preprint, 2017.
• Schumacher, A., Pireddu, L., Kallio, A., Niemenmaa, M., Korpelainen, E., Zanetti, G., and Heljanko, K.: Scripting for large-scale sequencing based on Hadoop. EMBnet.journal, volume 19.A: 84-85, 2013. Poster Abstract from The Next NGS Challenge Conference: Data Processing and Integration, 14-16 May 2013, Valencia, Spain.
• 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.