Keijo Heljanko
Assoc. Prof., Computer Science at Aalto University School of Business
Schools
- Aalto University School of Business
Links
Biography
Aalto University School of Business
Peer-reviewed scientific articles
Journal article-refereed, Original researchViraPipe: Scalable Parallel Pipeline for Viral Metagenome Analysis from Next Generation Sequencing Reads
Maarala, Altti; Bzhalava, Zurab; Dillner, Joakim; Heljanko, Keijo; Bzhalava, Davit2017 in BIOINFORMATICS (OXFORD UNIV PRESS INC)ISSN: 1367-4803Minimizing test suites with unfoldings of multithreaded programs
Saarikivi, Olli; Ponce de Leon, Hernan; Kähkönen, Kari; Heljanko, Keijo; Esparza, Javier2017 in ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS (Association for Computing Machinery (ACM))ISSN: 1539-9087When do we not need complex assume-guarantee rules?
Siirtola, Antti; Tripakis, Stavros; Heljanko, Keijo2017 in ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS (Association for Computing Machinery (ACM))ISSN: 1539-9087Hardware 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, Keijo2016 in JOURNAL OF SATISFIABILITY, BOOLEAN MODELING AND COMPUTATION (Association for Computing Machinery (ACM))ISSN: 1875-5011Synchronous counting and computational algorithm design
Dolev, Danny; Heljanko, Keijo; Järvisalo, Matti; Korhonen, Janne; Lenzen, Christoph; Rybicki, Joel; Suomela, Jukka; Wieringa, Siert2016 in JOURNAL OF COMPUTER AND SYSTEM SCIENCES (Academic Press Inc.)ISSN: 0022-0000LCTD Test-guided proofs for C programs on LLVM
Saarikivi, Olli; Heljanko, Keijo2016 in Journal of Logical and Algebraic Methods in Programming (Elsevier BV)ISSN: 2352-2208Unfolding based automated testing of multithreaded programs
Kahkonen, Kari; Saarikivi, Olli; Heljanko, Keijo2015 in AUTOMATED SOFTWARE ENGINEERING (Springer Netherlands)ISSN: 0928-8910Verifying large modular systems using iterative abstraction refinement
Lahtinen, Jussi; Kuismin, Tuomas; Heljanko, Keijo2015 in RELIABILITY ENGINEERING AND SYSTEM SAFETY (Elsevier Limited)ISSN: 0951-8320Parametrised modal interface automata
Siirtola, Antti; Heljanko, Keijo2015 in ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS (Association for Computing Machinery (ACM))ISSN: 1539-9087A symbolic model checking approach to verifying satellite onboard software
Gan, Xiang; Dubrovin, Jori; Heljanko, Keijo2014 in SCIENCE OF COMPUTER PROGRAMMING (Elsevier)ISSN: 0167-6423SeqPig: Simple and scalable scripting for large sequencing data sets in Hadoop
Schumacher, Andre; Pireddu, Luca; Niemenmaa, Matti; Kallio, Aleksi; Korpelainen, Eija; Zanetti, Gianluigi; Heljanko, Keijo2014 in BIOINFORMATICS (OXFORD UNIV PRESS INC)ISSN: 1367-4803LCT: A Parallel Distributed Testing Tool for Multithreaded Java Programs
Kähkönen, Kari; Saarikivi, Olli; Heljanko, Keijo2013 in ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE (Elsevier)ISSN: 1571-0661Exploiting step semantics for efficient bounded model checking of asynchronous systems
Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo2012 in SCIENCE OF COMPUTER PROGRAMMING (Elsevier)ISSN: 0167-6423Solving Parity Games by a Reduction to SAT
Heljanko, Keijo; Keinänen, Misa; Lange, Martin; Niemelä, Ilkka2012 in JOURNAL OF COMPUTER AND SYSTEM SCIENCES (Academic Press Inc.)ISSN: 0022-0000Model Checking of Safety-Critical Software in the Nuclear Engineering Domain
Lahtinen, Jussi; Valkonen, Janne; Björkman, Kim; Frits, Juho; Niemelä, Ilkka; Heljanko, Keijo2012 in RELIABILITY ENGINEERING AND SYSTEM SAFETY (Elsevier Limited)ISSN: 0951-8320Hadoop-BAM: Directly manipulating next generation sequencing data in the cloud
Niemenmaa, Matti; Kallio, Aleksi; Schumacher, André; Klemelä, Petri; Korpelainen, Eija; Heljanko, Keijo2012 in BIOINFORMATICS (OXFORD UNIV PRESS INC)ISSN: 1367-4803Efficient Model Checking of PSL Safety Properties
Launiainen, Tuomas; Heljanko, Keijo; Junttila, Tommi2011 in IET COMPUTERS AND DIGITAL TECHNIQUES (Institution of Engineering and Technology)ISSN: 1751-8601Linear Encodings of Bounded LTL Model Checking
Biere, Armin; Heljanko, Keijo; Junttila, Tommi; Latvala, Timo; Schuppan, Viktor2006 in LOGICAL METHODS IN COMPUTER SCIENCE (Technischen Universitat Braunschweig)Planning as satisfiability: parallel plans and algorithms for plan search
Rintanen, Jussi; Heljanko, Keijo; Niemelä, Ilkka2006 in ARTIFICIAL INTELLIGENCE (ELSEVIER SCIENCE BV)ISSN: 0004-3702BMC via on-the-fly Determinization
Jussila, Toni; Heljanko, Keijo; Niemelä, Ilkka2005 in Journal on Software Tools for Technology Transfer (ELSEVIER SCIENCE BV)ISSN: 1443-2779Bounded LTL Model Checking with Stable Models
Heljanko, Keijo; Niemelä, Ilkka2003 in THEORY AND PRACTICE OF LOGIC PROGRAMMING (Cambridge University Press)BMC via on-the-fly Determinization
Jussila, Toni; Heljanko, Keijo; Niemelä, Ilkka2003 in ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE (Elsevier)Testing LTL Formula Translation into Büchi Automata
Tauriainen, Heikki; Heljanko, Keijo2002 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)
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 booksPetri Net Analysis and Nonmonotonic Reasoning
Heljanko, K.; Niemelä, I.2000
Petri Net Analysis and Nonmonotonic Reasoning
Heljanko, K.; Niemelä, I.
2000 Conference proceedingsPortability analysis for weak memory models porthos One tool for all models
Ponce-de-León, Hernán; Furbach, Florian; Heljanko, Keijo; Meyer, Roland2017 in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Springer-Verlag)ISBN: 9783319667058ISSN: 0302-9743Assessing Big Data SQL Frameworks for Analyzing Event Logs
Hinkka, Markku; Lehto, Teemu; Heljanko, Keijo2016 ISBN: 9781467387750LCTD Tests-guided proofs for C programs on LLVM
Saarikivi, Olli; Heljanko, Keijo2016 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-2ISSN: 0302-9743Unfolding-Based Process Discovery
Ponce de León, Hernán; Rodríguez, César; Carmona, Josep; Heljanko, Keijo; Haar, Stefan2015 ISBN: 978-3-319-24952-0Unfolding based Minimal Test Suites for Testing Multithreaded Programs
Ponce-de-León, Hernán; Saarikivi, Olli; Kähkönen, Kari; Heljanko, Keijo; Esparza, Javier2015 ISSN: 1550-4808Reporting Races in Dynamic Partial Order Reduction
Saarikivi, Olli; Heljanko, Keijo2015 ISSN: 0302-9743When Do We (Not) Need Complex Assume-Guarantee Rules?
Siirtola, Antti Tapani; Tripakis, Stavros; Heljanko, Keijo2015 ISSN: 1550-4808Testing multithreaded programs with contextual unfoldings and dynamic symbolic execution
Kähkönen, Kari; Heljanko, Keijo2014 in International Conference on Application of Concurrency to System Design. Proceedings (IEEE)ISBN: 978-1-4799-4281-7 ISSN: 1550-4808Lightweight State Capturing for Automated Testing of Multithreaded Programs
Kähkönen, Kari; Heljanko, Keijo2014 ISBN: 978-3-319-09098-6Increasing Confidence in Liveness Model Checking Results with Proofs
Kuismin, Tuomas; Heljanko, Keijo2013 ISBN: 978-3-319-03076-0Parametrised Compositional Verification with Multiple Process and Data Types
Siirtola, Antti; Heljanko, Keijo2013 ISBN: 978-0-7695-5035-0Asynchronous Multi-core Incremental SAT Solving
Wieringa, Siert; Heljanko, Keijo2013 ISBN: 978-3-642-36741-0Concurrent Clause Strengthening
Wieringa, Siert; Heljanko, Keijo2013 ISBN: 978-3-642-39070-8A Symbolic Model Checking Approach to Verifying Satellite Onboard Software
Gan, Xiang; Dubrovin, Jori; Heljanko, Keijo2012 ISSN: 1863-2122Using Unfoldings in Automated Testing of Multithreaded Programs
Kähkönen, Kari; Saarikivi, Olli; Heljanko, Keijo2012 ISBN: 978-1-4503-1204-2Improving Dynamic Partial Order Reductions for Concolic Testing
Saarikivi, Olli; Kähkönen, Kari; Heljanko, Keijo2012 ISBN: 978-0-7695-4709-1LCT: An Open Source Concolic Testing Tool for Java Programs
Kähkönen, Kari; Launiainen, Tuomas; Saarikivi, Olli; Kauttio, Janne; Heljanko, Keijo; Niemelä, Ilkka2011 Hadoop-BAM: A Library for Genomic Data Processing
Niemenmaa, Matti; Schumacher, André; Heljanko, Keijo; Kallio, Aleksi; Klemelä, Petri; Hupponen, Taavi; Korpelainen, Eija2011 Experimental Comparison of Concolic and Random Testing for Java Card Applets
Kähkönen, Kari; Kindermann, Roland; Heljanko, Keijo; Niemelä, Ilkka2010 in Lecture Notes in Computer Science (IEEE COMPUTER SOCIETY PRESS)ISBN: 978-3-642-16163-6ISSN: 0302-9743Efficient Model Checking of PSL Safety Properties
Launiainen, Tuomas; Heljanko, Keijo; Junttila, Tommi2010 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ä, Ilkka2009 in Lecture Notes in Computer Science (SPRINGER)ISBN: 978-3-642-04693-3ISSN: 0302-9743Formal 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, Keijo2009 Analyzing Context-Free Grammars Using an Incremental SAT Solver
Axelsson, Roland; Heljanko, Keijo; Lange, Martin2008 Symbolic Step Encodings for Object Based Communicating State Machines
Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo2008 ISBN: 978-3-540-68862-4ISSN: 0302-9743Bounded Model Checking for Weak Alternating Buchi Automata
Heljanko, Keijo; Junttila, Tommi; Keinänen, Misa; Lange, Martin; Latvala, Timo2006 ISBN: 3-540-37406-XISSN: 0302-9743Incremental and Complete Bounded Model Checking for Full PLTL
Heljanko, Keijo; Junttila, Tommi; Latvala, TImo2005 Complexity Results for Checking Distributed Implementability
Heljanko, Keijo; Stefanescu, Alin2005 ISBN: 0-7695-2363-3ISSN: 1550-4808Simple is Better: Efficient Bounded Model Checking for Past LTL
Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi2005 ISBN: 3-540-24297-XSimple Bounded LTL Model Checking
Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi2004 ISBN: 3-540-23738-0Specification Coverage Aided Test Selection
Pyhälä, Tuomo; Heljanko, Keijo2003 ISBN: 0-7695-1887-7Parallelisation of the Petri Net Unfolding Algorithm.
Heljanko, K.; Khomenko, V.; Koutny, M.2002 Implementing LTL Model Checking with Net Unfoldings
Esparza, Javier; Heljanko, Keijo2001 Bounded Reachability Checking with Process Semantics
Heljanko, Keijo2001 Bounded LTL Model Checking with Stable Models
Heljanko, Keijo; Niemelä, Ilkka2001 Answer Set Programming and Bounded Model Checking
Heljanko, Keijo; Niemelä, Ilkka2001 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, Keijo1996 An Advanced Tool for Efficient Reachability Analysis
Varpaaniemi, K.; Lilius, J.; Heljanko, K.1996
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 articlesScripting for large-scale sequencing based on Hadoop
Schumacher, André; Pireddu, Luca; Kallio, Aleksi; Niemenmaa, Matti; Korpelainen, Eija; Zanetti, Gianluigi; Heljanko, Keijo2013 in EMBnet.journal (Humboldt University)ISSN: 2226-6089
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)
BookUnfoldings - A Partial Order Approach to Model Checking
Esparza, Javier; Heljanko, Keijo2008 ISBN: 978-3-540-77425-9
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, Nigel2013 Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD 2012)
Brandt, Jens; Heljanko, Keijo2012 ISBN: 978-1-4673-1687-3Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation
Barnat, Jiri; Heljanko, Keijo2011
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 reportModel Checking Methodology for Large Systems, Faults and Asynchronous Behaviour - {SARANA} 2011 Work Report
Lahtinen, Jussi; Launiainen, Tuomas; Heljanko, Keijo; Ropponen, Jonathan2012 Model-Based Analysis of a Stepwise Shutdown Logic
Björkman, Kim; Frits, Juho; Valkonen, Janne; Heljanko, Keijo; Niemelä, Ilkka2009 Interface Specification Methods for Software Components
Lampinen, Jani; Liedes, Sami; Kähkönen, Kari; Kauttio, Janne; Heljanko, Keijo2009 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ä, Ilkka2008 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ä, Ilkka2008 Symbolic Step Encodings for Object Based Communicating State Machines
Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo2007 Planning as Satisfiability: Parallel Plans and Algorithms for Plan Search
Rintanen, Jussi; Heljanko, Keijo; Niemelä, Ilkka2005 Complexity Results for Checking Distributed Implementability
Heljanko, Keijo; Stefanescu, Alin2004 Simple bounded LTL model checking
Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi2004 Parallel encodings of classical planning as satisfiability
Rintanen, Jussi; Heljanko, Keijo; Niemelä, Ilkka2004 Implementing LTL Model Checking with Net Unfoldings
Esparza, Javier; Heljanko, Keijo2001 Parallelisation of the Petri Net Unfolding Algorithm
Heljanko, Keijo; Khomenko, Victor; Koutny, Maciej2001 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
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 applicationsPROD 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, Pauli2004 Bomotest - A formal conformance testing tool, Version 1.5
Pyhälä, Tuomo; Heljanko, Keijo2003 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, Pauli2001 unfsmodels 0.9: an LTL model checker using net unfoldings
Heljanko, Keijo; Simons, Patrik2001 boundsmodels 0.9: a bounded LTL model checker
Heljanko, Keijo; Simons, Patrik2001 punroll 0.3: a bounded reachability checker
Heljanko, Keijo2001 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
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 Videos
Hadoop-BAM and SeqPig - Keijo Heljanko, Aalto University, Finland
Read about executive education
Other experts
Looking for an expert?
Contact us and we'll find the best option for you.