HeljankoAalto-yliopisto

Keijo Heljanko

Professori, taso 1, Tietotekniikka, erityisesti ohjemistojärjestelmien ja ohjelmistotuotannon alue, Tietotekniikan laitos


Tämä henkilö ResearcherID.com sivustolla.

Yhteystiedot

Huonenumero
A320
Työsähköpostiosoite
keijo.heljanko at aalto.fi
Työmatkapuhelin
+358 50 3084 871
Skype
Soita | Lisää kontaktiksi
Web- sivu

Julkaisut

Vertaisarvioidut tieteelliset artikkelit

Alkuperäisartikkeli tieteellisessä aikakauslehdessä

Minimizing test suites with unfoldings of multithreaded programs

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

2017 

ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS 

ISSN: 1539-9087 

When do we not need complex assume-guarantee rules?

Siirtola, Antti; Tripakis, Stavros; Heljanko, Keijo 

2017 

ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS 

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 

JOURNAL OF SATISFIABILITY, BOOLEAN MODELING AND COMPUTATION 

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 

JOURNAL OF COMPUTER AND SYSTEM SCIENCES 

ISSN: 0022-0000 

LCTD Test-guided proofs for C programs on LLVM

Saarikivi, Olli; Heljanko, Keijo 

2016 

Journal of Logical and Algebraic Methods in Programming 

Unfolding based automated testing of multithreaded programs

Kahkonen, Kari; Saarikivi, Olli; Heljanko, Keijo 

2015 

AUTOMATED SOFTWARE ENGINEERING 

ISSN: 0928-8910 

Verifying large modular systems using iterative abstraction refinement

Lahtinen, Jussi; Kuismin, Tuomas; Heljanko, Keijo 

2015 

RELIABILITY ENGINEERING AND SYSTEM SAFETY 

ISSN: 0951-8320 

Parametrised modal interface automata

Siirtola, Antti; Heljanko, Keijo 

2015 

ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS 

ISSN: 1539-9087 

A symbolic model checking approach to verifying satellite onboard software

Gan, Xiang; Dubrovin, Jori; Heljanko, Keijo 

2014 

SCIENCE OF COMPUTER PROGRAMMING 

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 

BIOINFORMATICS 

ISSN: 1367-4803 

LCT: A Parallel Distributed Testing Tool for Multithreaded Java Programs

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

2013 

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 

ISSN: 1571-0661 

Exploiting step semantics for efficient bounded model checking of asynchronous systems

Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo 

2012 

SCIENCE OF COMPUTER PROGRAMMING 

ISSN: 0167-6423 

Solving Parity Games by a Reduction to SAT

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

2012 

JOURNAL OF COMPUTER AND SYSTEM SCIENCES 

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 

RELIABILITY ENGINEERING AND SYSTEM SAFETY 

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 

BIOINFORMATICS 

ISSN: 1367-4803 

Efficient Model Checking of PSL Safety Properties

Launiainen, Tuomas; Heljanko, Keijo; Junttila, Tommi 

2011 

IET COMPUTERS AND DIGITAL TECHNIQUES 

ISSN: 1751-8601 

Linear Encodings of Bounded LTL Model Checking

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

2006 

LOGICAL METHODS IN COMPUTER SCIENCE 

Planning as satisfiability: parallel plans and algorithms for plan search

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

2006 

ARTIFICIAL INTELLIGENCE 

ISSN: 0004-3702 

BMC via on-the-fly Determinization

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

2005 

Journal on Software Tools for Technology Transfer 

ISSN: 1443-2779 

Bounded LTL Model Checking with Stable Models

Heljanko, Keijo; Niemelä, Ilkka 

2003 

THEORY AND PRACTICE OF LOGIC PROGRAMMING 

BMC via on-the-fly Determinization

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

2003 

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 

Testing LTL Formula Translation into Büchi Automata

Tauriainen, Heikki; Heljanko, Keijo 

2002 

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER 

Coping with Strong Fairness

Latvala, T.; Heljanko, K. 

2000 

FUNDAMENTA INFORMATICAE 

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

Heljanko, K. 

1999 

FUNDAMENTA INFORMATICAE 

Kirjan tai muun kokoomateoksen osa

Petri Net Analysis and Nonmonotonic Reasoning

Heljanko, K.; Niemelä, I. 

2000 

Helsinki University of Technology 

Artikkeli konferenssijulkaisussa

Assessing Big Data SQL Frameworks for Analyzing Event Logs

Hinkka, Markku; Lehto, Teemu; Heljanko, Keijo 

2016 

Institute of Electrical and Electronics Engineers Inc. 

ISBN: 9781467387750 

LCTD Tests-guided proofs for C programs on LLVM

Saarikivi, Olli; Heljanko, Keijo 

2016 

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 

SPRINGER 

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 

IEEE 

ISSN: 1550-4808 

Reporting Races in Dynamic Partial Order Reduction

Saarikivi, Olli; Heljanko, Keijo 

2015 

Springer-verlag Berlin 

ISSN: 0302-9743 

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

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

2015 

IEEE Computer Society 

ISSN: 1550-4808 

Testing multithreaded programs with contextual unfoldings and dynamic symbolic execution

Kähkönen, Kari; Heljanko, Keijo 

2014 

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 

IEEE COMPUTER SOCIETY PRESS 

ISBN: 978-0-7695-5035-0 

Asynchronous Multi-core Incremental SAT Solving

Wieringa, Siert; Heljanko, Keijo 

2013 

SPRINGER GABLER 

ISBN: 978-3-642-36741-0 

Concurrent Clause Strengthening

Wieringa, Siert; Heljanko, Keijo 

2013 

SPRINGER GABLER 

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 

ASSOCIATION FOR COMPUTING MACHINERY 

ISBN: 978-1-4503-1204-2 

Improving Dynamic Partial Order Reductions for Concolic Testing

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

2012 

IEEE COMPUTER SOCIETY PRESS 

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 

Lecture Notes in Computer Science 

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 

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 

SPRINGER 

Symbolic Step Encodings for Object Based Communicating State Machines

Dubrovin, Jori; Junttila, Tommi; Heljanko, Keijo 

2008 

SPRINGER GABLER 

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 

SPRINGER 

ISBN: 3-540-37406-X 

ISSN: 0302-9743 

Incremental and Complete Bounded Model Checking for Full PLTL

Heljanko, Keijo; Junttila, Tommi; Latvala, TImo 

2005 

SPRINGER 

Complexity Results for Checking Distributed Implementability

Heljanko, Keijo; Stefanescu, Alin 

2005 

IEEE Computer Society 

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 

SPRINGER 

ISBN: 3-540-24297-X 

Simple Bounded LTL Model Checking

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

2004 

SPRINGER 

ISBN: 3-540-23738-0 

Specification Coverage Aided Test Selection

Pyhälä, Tuomo; Heljanko, Keijo 

2003 

IEEE Computer Society 

ISBN: 0-7695-1887-7 

Parallelisation of the Petri Net Unfolding Algorithm.

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

2002 

SPRINGER 

Implementing LTL Model Checking with Net Unfoldings

Esparza, Javier; Heljanko, Keijo 

2001 

SPRINGER 

Bounded LTL Model Checking with Stable Models

Heljanko, Keijo; Niemelä, Ilkka 

2001 

SPRINGER 

Answer Set Programming and Bounded Model Checking

Heljanko, Keijo; Niemelä, Ilkka 

2001 

AAAI PRESS 

Bounded Reachability Checking with Process Semantics

Heljanko, Keijo 

2001 

SPRINGER 

A New Unfolding Approach to LTL Model Checking

Esparza, J.; Heljanko, K. 

2000 

SPRINGER 

Model Checking with Finite Complete Prefixes is PSPACE-Complete

Heljanko, K. 

2000 

SPRINGER 

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

Tauriainen, H.; Heljanko, K. 

2000 

SPRINGER 

Minimizing Finite Complete Prefixes

Heljanko, K. 

1999 

Warsaw University 

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

Heljanko, K. 

1999 

SPRINGER 

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

Latvala, T.; Heljanko, K. 

1999 

Warsaw University 

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

Heljanko, K. 

1998 

Humboldt-Universitat zu Berlin 

PROD-3.2-An Advanced Tool for Efficient Reachability Analysis

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

1997 

SPRINGER 

Implementing a CTL Model Checker

Heljanko, Keijo 

1996 

Humboldt University 

An Advanced Tool for Efficient Reachability Analysis

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

1996 

Vertaisarvioimattomat tieteelliset kirjoitukset

Kirjoitus tieteellisessä aikakauslehdessä

Scripting for large-scale sequencing based on Hadoop

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

2013 

EMBnet.journal 

ISSN: 2226-6089 

Tieteelliset kirjat (monografiat)

Kustannettu tieteellinen erillisteos

Unfoldings - A Partial Order Approach to Model Checking

Esparza, Javier; Heljanko, Keijo 

2008 

SPRINGER GABLER 

ISBN: 978-3-540-77425-9 

Toimitettu kirja, kokoomateos, konferenssijulkaisu tai lehden erikoisnumero

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 

Elsevier 

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

Brandt, Jens; Heljanko, Keijo 

2012 

IEEE 

ISBN: 978-1-4673-1687-3 

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

Barnat, Jiri; Heljanko, Keijo 

2011 

Electronic Proceedings in Theoretical Computer Science 

Ammattiyhteisölle suunnatut julkaisut

Julkaistu kehittämis- tai tutkimusraportti taikka -selvitys

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 

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 

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 

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 

Audiovisuaaliset aineistot ja tieto- ja viestintätekniset ohjelmat

Tieto- ja viestintätekniset ohjelma tai ohjelmisto

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 

boundsmodels 0.9: a bounded LTL model checker

Heljanko, Keijo; Simons, Patrik 

2001 

punroll 0.3: a bounded reachability checker

Heljanko, Keijo 

2001 

unfsmodels 0.9: an LTL model checker using net unfoldings

Heljanko, Keijo; Simons, Patrik 

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 

Alert