Keijo Heljanko

Peer-reviewed scientific articles

Journal article-refereed, Original research

ViraPipe: Scalable Parallel Pipeline for Viral Metagenome Analysis from Next Generation Sequencing Reads

Maarala, Altti; Bzhalava, Zurab; Dillner, Joakim; Heljanko, Keijo; Bzhalava, Davit

2017 in BIOINFORMATICS (OXFORD UNIV PRESS INC)

ISSN: 1367-4803

Minimizing test suites with unfoldings of multithreaded programs

Saarikivi, Olli; Ponce de Leon, Hernan; Kähkönen, Kari; Heljanko, Keijo; Esparza, Javier

2017 in ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS (Association for Computing Machinery (ACM))

ISSN: 1539-9087

When do we not need complex assume-guarantee rules?

Siirtola, Antti; Tripakis, Stavros; Heljanko, Keijo

2017 in ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS (Association for Computing Machinery (ACM))

ISSN: 1539-9087

Hardware model checking competition 2014: An analysis and comparison of solvers and benchmarks

Cabodi, Gianpiero; Loiacono, Carmelo; Palena, Marco; Pasini, Paolo; Patti, Denis; Quer, Stefano; Vendraminetto, Danilo; Biere, Armin; Heljanko, Keijo

2016 in JOURNAL OF SATISFIABILITY, BOOLEAN MODELING AND COMPUTATION (Association for Computing Machinery (ACM))

ISSN: 1875-5011

Synchronous counting and computational algorithm design

Dolev, Danny; Heljanko, Keijo; Järvisalo, Matti; Korhonen, Janne; Lenzen, Christoph; Rybicki, Joel; Suomela, Jukka; Wieringa, Siert

2016 in JOURNAL OF COMPUTER AND SYSTEM SCIENCES (Academic Press Inc.)

ISSN: 0022-0000

LCTD Test-guided proofs for C programs on LLVM

Saarikivi, Olli; Heljanko, Keijo

2016 in Journal of Logical and Algebraic Methods in Programming (Elsevier BV)

ISSN: 2352-2208

Unfolding based automated testing of multithreaded programs

Kahkonen, Kari; Saarikivi, Olli; Heljanko, Keijo

2015 in AUTOMATED SOFTWARE ENGINEERING (Springer Netherlands)

ISSN: 0928-8910

Verifying large modular systems using iterative abstraction refinement

Lahtinen, Jussi; Kuismin, Tuomas; Heljanko, Keijo

2015 in RELIABILITY ENGINEERING AND SYSTEM SAFETY (Elsevier Limited)

ISSN: 0951-8320

Parametrised modal interface automata

Siirtola, Antti; Heljanko, Keijo

2015 in ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS (Association for Computing Machinery (ACM))

ISSN: 1539-9087

A symbolic model checking approach to verifying satellite onboard software

Gan, Xiang; Dubrovin, Jori; Heljanko, Keijo

2014 in SCIENCE OF COMPUTER PROGRAMMING (Elsevier)

ISSN: 0167-6423

SeqPig: Simple and scalable scripting for large sequencing data sets in Hadoop

Schumacher, Andre; Pireddu, Luca; Niemenmaa, Matti; Kallio, Aleksi; Korpelainen, Eija; Zanetti, Gianluigi; Heljanko, Keijo

2014 in BIOINFORMATICS (OXFORD UNIV PRESS INC)

ISSN: 1367-4803

LCT: A Parallel Distributed Testing Tool for Multithreaded Java Programs

Kähkönen, Kari; Saarikivi, Olli; Heljanko, Keijo

2013 in ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE (Elsevier)

ISSN: 1571-0661

Exploiting step semantics for efficient bounded model checking of asynchronous systems

Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo

2012 in SCIENCE OF COMPUTER PROGRAMMING (Elsevier)

ISSN: 0167-6423

Solving Parity Games by a Reduction to SAT

Heljanko, Keijo; Keinänen, Misa; Lange, Martin; Niemelä, Ilkka

2012 in JOURNAL OF COMPUTER AND SYSTEM SCIENCES (Academic Press Inc.)

ISSN: 0022-0000

Model Checking of Safety-Critical Software in the Nuclear Engineering Domain

Lahtinen, Jussi; Valkonen, Janne; Björkman, Kim; Frits, Juho; Niemelä, Ilkka; Heljanko, Keijo

2012 in RELIABILITY ENGINEERING AND SYSTEM SAFETY (Elsevier Limited)

ISSN: 0951-8320

Hadoop-BAM: Directly manipulating next generation sequencing data in the cloud

Niemenmaa, Matti; Kallio, Aleksi; Schumacher, André; Klemelä, Petri; Korpelainen, Eija; Heljanko, Keijo

2012 in BIOINFORMATICS (OXFORD UNIV PRESS INC)

ISSN: 1367-4803

Efficient Model Checking of PSL Safety Properties

Launiainen, Tuomas; Heljanko, Keijo; Junttila, Tommi

2011 in IET COMPUTERS AND DIGITAL TECHNIQUES (Institution of Engineering and Technology)

ISSN: 1751-8601

Linear Encodings of Bounded LTL Model Checking

Biere, Armin; Heljanko, Keijo; Junttila, Tommi; Latvala, Timo; Schuppan, Viktor

2006 in LOGICAL METHODS IN COMPUTER SCIENCE (Technischen Universitat Braunschweig)

Planning as satisfiability: parallel plans and algorithms for plan search

Rintanen, Jussi; Heljanko, Keijo; Niemelä, Ilkka

2006 in ARTIFICIAL INTELLIGENCE (ELSEVIER SCIENCE BV)

ISSN: 0004-3702

BMC via on-the-fly Determinization

Jussila, Toni; Heljanko, Keijo; Niemelä, Ilkka

2005 in Journal on Software Tools for Technology Transfer (ELSEVIER SCIENCE BV)

ISSN: 1443-2779

Bounded LTL Model Checking with Stable Models

Heljanko, Keijo; Niemelä, Ilkka

2003 in THEORY AND PRACTICE OF LOGIC PROGRAMMING (Cambridge University Press)

BMC via on-the-fly Determinization

Jussila, Toni; Heljanko, Keijo; Niemelä, Ilkka

2003 in ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE (Elsevier)

Testing LTL Formula Translation into Büchi Automata

Tauriainen, Heikki; Heljanko, Keijo

2002 in INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER (Springer Verlag)

Coping with Strong Fairness

Latvala, T.; Heljanko, K.

2000 in FUNDAMENTA INFORMATICAE (IOS PRESS)

Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-safe Petri Nets

Heljanko, K.

1999 in FUNDAMENTA INFORMATICAE (IOS PRESS)

Book section, Chapters in research books

Petri Net Analysis and Nonmonotonic Reasoning

Heljanko, K.; Niemelä, I.

2000

Conference proceedings

Portability analysis for weak memory models porthos One tool for all models

Ponce-de-León, Hernán; Furbach, Florian; Heljanko, Keijo; Meyer, Roland

2017 in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Springer-Verlag)

ISBN: 9783319667058

ISSN: 0302-9743

Assessing Big Data SQL Frameworks for Analyzing Event Logs

Hinkka, Markku; Lehto, Teemu; Heljanko, Keijo

2016

ISBN: 9781467387750

LCTD Tests-guided proofs for C programs on LLVM

Saarikivi, Olli; Heljanko, Keijo

2016 in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Springer-Verlag)

ISBN: 978-3-662-49673-2

ISSN: 0302-9743

Unfolding-Based Process Discovery

Ponce de León, Hernán; Rodríguez, César; Carmona, Josep; Heljanko, Keijo; Haar, Stefan

2015

ISBN: 978-3-319-24952-0

Unfolding based Minimal Test Suites for Testing Multithreaded Programs

Ponce-de-León, Hernán; Saarikivi, Olli; Kähkönen, Kari; Heljanko, Keijo; Esparza, Javier

2015

ISSN: 1550-4808

Reporting Races in Dynamic Partial Order Reduction

Saarikivi, Olli; Heljanko, Keijo

2015

ISSN: 0302-9743

When Do We (Not) Need Complex Assume-Guarantee Rules?

Siirtola, Antti Tapani; Tripakis, Stavros; Heljanko, Keijo

2015

ISSN: 1550-4808

Testing multithreaded programs with contextual unfoldings and dynamic symbolic execution

Kähkönen, Kari; Heljanko, Keijo

2014 in International Conference on Application of Concurrency to System Design. Proceedings (IEEE)

ISBN: 978-1-4799-4281-7

ISSN: 1550-4808

Lightweight State Capturing for Automated Testing of Multithreaded Programs

Kähkönen, Kari; Heljanko, Keijo

2014

ISBN: 978-3-319-09098-6

Increasing Confidence in Liveness Model Checking Results with Proofs

Kuismin, Tuomas; Heljanko, Keijo

2013

ISBN: 978-3-319-03076-0

Parametrised Compositional Verification with Multiple Process and Data Types

Siirtola, Antti; Heljanko, Keijo

2013

ISBN: 978-0-7695-5035-0

Asynchronous Multi-core Incremental SAT Solving

Wieringa, Siert; Heljanko, Keijo

2013

ISBN: 978-3-642-36741-0

Concurrent Clause Strengthening

Wieringa, Siert; Heljanko, Keijo

2013

ISBN: 978-3-642-39070-8

A Symbolic Model Checking Approach to Verifying Satellite Onboard Software

Gan, Xiang; Dubrovin, Jori; Heljanko, Keijo

2012

ISSN: 1863-2122

Using Unfoldings in Automated Testing of Multithreaded Programs

Kähkönen, Kari; Saarikivi, Olli; Heljanko, Keijo

2012

ISBN: 978-1-4503-1204-2

Improving Dynamic Partial Order Reductions for Concolic Testing

Saarikivi, Olli; Kähkönen, Kari; Heljanko, Keijo

2012

ISBN: 978-0-7695-4709-1

LCT: An Open Source Concolic Testing Tool for Java Programs

Kähkönen, Kari; Launiainen, Tuomas; Saarikivi, Olli; Kauttio, Janne; Heljanko, Keijo; Niemelä, Ilkka

2011

Hadoop-BAM: A Library for Genomic Data Processing

Niemenmaa, Matti; Schumacher, André; Heljanko, Keijo; Kallio, Aleksi; Klemelä, Petri; Hupponen, Taavi; Korpelainen, Eija

2011

Experimental Comparison of Concolic and Random Testing for Java Card Applets

Kähkönen, Kari; Kindermann, Roland; Heljanko, Keijo; Niemelä, Ilkka

2010 in Lecture Notes in Computer Science (IEEE COMPUTER SOCIETY PRESS)

ISBN: 978-3-642-16163-6

ISSN: 0302-9743

Efficient Model Checking of PSL Safety Properties

Launiainen, Tuomas; Heljanko, Keijo; Junttila, Tommi

2010

Verification of Safety Logic Designs by Model Checking

Björkman, Kim; Frits, Juho; Valkonen, Janne; Lahtinen, Jussi; Heljanko, Keijo; Niemelä, Ilkka; Hämäläinen, Jari J.

2009

The LIME Interface Specification Language and Runtime Monitoring Tool

Kähkönen, Kari; Lampinen, Jani; Heljanko, Keijo; Niemelä, Ilkka

2009 in Lecture Notes in Computer Science (SPRINGER)

ISBN: 978-3-642-04693-3

ISSN: 0302-9743

Formal Verification of Safety Automation Logic Designs

Valkonen, Janne; Koskimies, Matti; Björkman, Kim; Heljanko, Keijo; Niemelä, Ilkka; Hämäläinen, Jari J.

2009

Tarmo: A framework for Parallelized Bounded Model Checking

Wieringa, Siert; Niemenmaa, Matti; Heljanko, Keijo

2009

Analyzing Context-Free Grammars Using an Incremental SAT Solver

Axelsson, Roland; Heljanko, Keijo; Lange, Martin

2008

Symbolic Step Encodings for Object Based Communicating State Machines

Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo

2008

ISBN: 978-3-540-68862-4

ISSN: 0302-9743

Bounded Model Checking for Weak Alternating Buchi Automata

Heljanko, Keijo; Junttila, Tommi; Keinänen, Misa; Lange, Martin; Latvala, Timo

2006

ISBN: 3-540-37406-X

ISSN: 0302-9743

Incremental and Complete Bounded Model Checking for Full PLTL

Heljanko, Keijo; Junttila, Tommi; Latvala, TImo

2005

Complexity Results for Checking Distributed Implementability

Heljanko, Keijo; Stefanescu, Alin

2005

ISBN: 0-7695-2363-3

ISSN: 1550-4808

Simple is Better: Efficient Bounded Model Checking for Past LTL

Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi

2005

ISBN: 3-540-24297-X

Simple Bounded LTL Model Checking

Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi

2004

ISBN: 3-540-23738-0

Specification Coverage Aided Test Selection

Pyhälä, Tuomo; Heljanko, Keijo

2003

ISBN: 0-7695-1887-7

Parallelisation of the Petri Net Unfolding Algorithm.

Heljanko, K.; Khomenko, V.; Koutny, M.

2002

Implementing LTL Model Checking with Net Unfoldings

Esparza, Javier; Heljanko, Keijo

2001

Bounded Reachability Checking with Process Semantics

Heljanko, Keijo

2001

Bounded LTL Model Checking with Stable Models

Heljanko, Keijo; Niemelä, Ilkka

2001

Answer Set Programming and Bounded Model Checking

Heljanko, Keijo; Niemelä, Ilkka

2001

A New Unfolding Approach to LTL Model Checking

Esparza, J.; Heljanko, K.

2000

Model Checking with Finite Complete Prefixes is PSPACE-Complete

Heljanko, K.

2000

Testing SPIN's LTL Formula Conversion into Büchi Automata with Randomly Generated Input

Tauriainen, H.; Heljanko, K.

2000

Minimizing Finite Complete Prefixes

Heljanko, K.

1999

Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-safe Petri Nets

Heljanko, K.

1999

Coping with strong fairness - on-the-fly emptiness checking with Streett Automata

Latvala, T.; Heljanko, K.

1999

Deadlock Checking for Complete Finite Prefixes Using Logic Programs with Stable Model Semantics

Heljanko, K.

1998

PROD-3.2-An Advanced Tool for Efficient Reachability Analysis

Varpaaniemi, K.; Heljanko, K.; Lilius, J.

1997

Implementing a CTL Model Checker

Heljanko, Keijo

1996

An Advanced Tool for Efficient Reachability Analysis

Varpaaniemi, K.; Lilius, J.; Heljanko, K.

1996

Non-refereed scientific articles

Unrefereed journal articles

Scripting for large-scale sequencing based on Hadoop

Schumacher, André; Pireddu, Luca; Kallio, Aleksi; Niemenmaa, Matti; Korpelainen, Eija; Zanetti, Gianluigi; Heljanko, Keijo

2013 in EMBnet.journal (Humboldt University)

ISSN: 2226-6089

Scientific books (monographs)

Book

Unfoldings - A Partial Order Approach to Model Checking

Esparza, Javier; Heljanko, Keijo

2008

ISBN: 978-3-540-77425-9

Book (editor)

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 (PD

Bradley, Jeremy T.; Heljanko, Keijo; Knottenbelt, William J.; Thomas, Nigel

2013

Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD 2012)

Brandt, Jens; Heljanko, Keijo

2012

ISBN: 978-1-4673-1687-3

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

Barnat, Jiri; Heljanko, Keijo

2011

Publications intended for professional communities

Published development or research report

Model Checking Methodology for Large Systems, Faults and Asynchronous Behaviour - {SARANA} 2011 Work Report

Lahtinen, Jussi; Launiainen, Tuomas; Heljanko, Keijo; Ropponen, Jonathan

2012

Model-Based Analysis of a Stepwise Shutdown Logic

Björkman, Kim; Frits, Juho; Valkonen, Janne; Heljanko, Keijo; Niemelä, Ilkka

2009

Interface Specification Methods for Software Components

Lampinen, Jani; Liedes, Sami; Kähkönen, Kari; Kauttio, Janne; Heljanko, Keijo

2009

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

Valkonen, Janne; Koskimies, Matti; Pettersson, Ville; Heljanko, Keijo; Holmberg, Jan-Erik; Niemelä, Ilkka

2008

NPP Safety Automation Systems Analysis - State of the Art

Valkonen, Janne; Karanta, Ilkka; Koskimies, Matti; Heljanko, Keijo; Niemelä, Ilkka; Sheridan, Dan; Bloomfield, Robin E.

2008

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

Valkonen, Janne; Petterson, Ville; Björkman, Kim; Holmberg, Jan-Erik; Koskimies, Matti; Heljanko, Keijo; Niemelä, Ilkka

2008

Symbolic Step Encodings for Object Based Communicating State Machines

Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo

2007

Planning as Satisfiability: Parallel Plans and Algorithms for Plan Search

Rintanen, Jussi; Heljanko, Keijo; Niemelä, Ilkka

2005

Complexity Results for Checking Distributed Implementability

Heljanko, Keijo; Stefanescu, Alin

2004

Simple bounded LTL model checking

Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi

2004

Parallel encodings of classical planning as satisfiability

Rintanen, Jussi; Heljanko, Keijo; Niemelä, Ilkka

2004

Implementing LTL Model Checking with Net Unfoldings

Esparza, Javier; Heljanko, Keijo

2001

Parallelisation of the Petri Net Unfolding Algorithm

Heljanko, Keijo; Khomenko, Victor; Koutny, Maciej

2001

A New Unfolding Approach to LTL Model Checking

Esparza, J.; Heljanko, K.

2000

Deadlock and Reachability Checking with Finite Complete Prefixes

Heljanko, K.

1999

Model Checking the Branching Time Temporal Logic CTL

Heljanko, K.

1997

PROD 3.111 An Advanced Tool for Efficient Reachability Analysis

Varpaaniemi, K.; Lilius, J.; Heljanko, K.

1996

Audiovisual material, ICT software

ICT programs or applications

PROD 3.4.00 -saavutettavuusanalyysiohjelmisto

Anderson, Lasse; Helander, Johannes; Heljanko, Keijo; Janhunen, Tomi; Jürgens, Robert; Kangas, Ismo; Nurmela, Kari; Oksanen, Kenneth; Pesonen, Olavi; Rauhamaa, Marko; Reilly, James; Suonsivu, Heikki; Valkealahti, Kimmo; Varpaaniemi, Kimmo; Väisänen, Pauli

2004

Bomotest - A formal conformance testing tool, Version 1.5

Pyhälä, Tuomo; Heljanko, Keijo

2003

PROD 3.3.09 -saavutettavuusanalyysiohjelmisto

Anderson, Lasse; Helander, Johannes; Heljanko, Keijo; Janhunen, Tomi; Jürgens, Robert; Kangas, Ismo; Nurmela, Kari; Oksanen, Kenneth; Pesonen, Olavi; Rauhamaa, Marko; Reilly, James; Suonsivu, Heikki; Valkealahti, Kimmo; Varpaaniemi, Kimmo; Väisänen, Pauli

2001

unfsmodels 0.9: an LTL model checker using net unfoldings

Heljanko, Keijo; Simons, Patrik

2001

boundsmodels 0.9: a bounded LTL model checker

Heljanko, Keijo; Simons, Patrik

2001

punroll 0.3: a bounded reachability checker

Heljanko, Keijo

2001

PROD 3.3.08 -saavutettavuusanalyysiohjelmisto

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

2000