Keijo Heljanko

107 papers A* 5A 6B 15C 3Journal 40Unranked 33
YearRankTypeTitle / Venue / Authors
2025 — conf
Introducing Certificates to the Hardware Model Checking Competition.
CAV (1)
Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko
2025 C conf
Massively Parallel Computation of Matching Statistics.
SPIRE
Anastasia C. Diseth, Keijo Heljanko, Simon J. Puglisi
2025 J jnl
Scalable Domain-decomposed Monte Carlo Neutral Transport for Nuclear Fusion.
CoRR
Oskar Lappi, Huw Leggate, Yannick Marandet, Jan Åström, Keijo Heljanko, Dmitriy V. Borodin
2024 — conf
Certifying Phase Abstraction.
IJCAR (1)
Nils Froleyks, Emily Yu, Armin Biere, Keijo Heljanko
2024 J jnl
Certifying Phase Abstraction.
CoRR
Nils Froleyks, Emily Yu, Armin Biere, Keijo Heljanko
2024 J jnl
SOMA: Observability, monitoring, and in situ analytics for exascale applications.
Concurr. Comput. Pract. Exp.
Dewi Yokelson, Oskar Lappi, Srinivasan Ramesh, Miikka S. Väisälä, Kevin A. Huck, Touko Puro, Boyana Norris, Maarit J. Korpi-Lagg, Keijo Heljanko, Allen D. Malony
2024 A conf
Subsystem Discovery in High-Dimensional Time-Series Using Masked Autoencoders.
ECAI
Teemu Sarapisto, Haoyu Wei, Keijo Heljanko, Arto Klami, Laura Ruotsalainen
2024 — conf
Towards Unified Analysis of GPU Consistency.
ASPLOS (4)
Haining Tong, Natalia Gavrilenko, Hernán Ponce de León, Keijo Heljanko
2023 B conf
Towards Compositional Hardware Model Checking Certification.
FMCAD
Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko
2022 B conf
Stratified Certification for k-Induction.
FMCAD
Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko
2022 J jnl
Stratified Certification for k-Induction.
CoRR
Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko
2021 — conf
Progress in Certifying Hardware Model Checking Results.
CAV (2)
Emily Yu, Armin Biere, Keijo Heljanko
2020 J jnl
An optimal cut-off algorithm for parameterised refinement checking.
Sci. Comput. Program.
Antti Siirtola, Keijo Heljanko
2020 J jnl
CEFIoT: A Fault-Tolerant IoT Architecture for Edge and Cloud.
CoRR
Asad Javed, Keijo Heljanko, Andrea Buda, Kary Främling
2020 — conf
Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution).
TACAS (2)
Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer
2020 J jnl
IoTEF: A Federated Edge-Cloud Architecture for Fault-Tolerant IoT Applications.
J. Grid Comput.
Asad Javed, Jérémy Robert, Keijo Heljanko, Kary Främling
2020 J jnl
Reinforcement learning of adaptive online rescheduling timing and computing time allocation.
Comput. Chem. Eng.
Teemu J. Ikonen, Keijo Heljanko, Iiro Harjunkoski
2020 B conf
Scalable Reference Genome Assembly from Compressed Pan-Genome Index with Spark.
BigData
Altti Ilari Maarala, Ossi Arasalo, Daniel Valenzuela, Keijo Heljanko, Veli Mäkinen
2019 — conf
Access Time Improvement Framework for Standardized IoT Gateways.
PerCom Workshops
Asad Javed, Narges Yousefnezhad, Jérémy Robert, Keijo Heljanko, Kary Främling
2019 — conf
BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings.
CAV (1)
Natalia Gavrilenko, Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer
2019 C conf
Certifying Hardware Model Checking Results.
ICFEM
Zhengqi Yu, Armin Biere, Keijo Heljanko
2019 J jnl
Exploiting Event Log Data-Attributes in RNN Based Prediction.
CoRR
Markku Hinkka, Teemu Lehto, Keijo Heljanko
2019 — conf
Exploiting Event Log Event Attributes in RNN Based Prediction.
ADBIS (Short Papers and Workshops)
Markku Hinkka, Teemu Lehto, Keijo Heljanko
2019 — conf
Exploiting Event Log Event Attributes in RNN Based Prediction.
SIMPDA
Markku Hinkka, Teemu Lehto, Keijo Heljanko
2018 B conf
BMC with Memory Models as Modules.
FMCAD
Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer
2018 — conf
CEFIoT: A fault-tolerant IoT architecture for edge and cloud.
WF-IoT
Asad Javed, Keijo Heljanko, Andrea Buda, Kary Främling
2018 — conf
Classifying Process Instances Using Recurrent Neural Networks.
Business Process Management Workshops
Markku Hinkka, Teemu Lehto, Keijo Heljanko, Alexander Jung
2018 J jnl
Classifying Process Instances Using Recurrent Neural Networks.
CoRR
Markku Hinkka, Teemu Lehto, Keijo Heljanko, Alexander Jung
2018 — conf
Dynamic Cut-Off Algorithm for Parameterised Refinement Checking.
FACS
Antti Siirtola, Keijo Heljanko
2018 J jnl
Testing Programs with Contextual Unfoldings.
ACM Trans. Embed. Comput. Syst.
Kari Kähkönen, Keijo Heljanko
2018 J jnl
ViraPipe: scalable parallel pipeline for viral metagenome analysis from next generation sequencing reads.
Bioinform.
Altti Ilari Maarala, Zurab Bzhalava, Joakim Dillner, Keijo Heljanko, Davit Bzhalava
2017 B conf
Hardware model checking competition 2017.
FMCAD
Armin Biere, Tom van Dijk, Keijo Heljanko
2017 J jnl
Minimizing Test Suites with Unfoldings of Multithreaded Programs.
ACM Trans. Embed. Comput. Syst.
Olli Saarikivi, Hernán Ponce de León, Kari Kähkönen, Keijo Heljanko, Javier Esparza
2017 J jnl
Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all Models.
CoRR
Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer
2017 B conf
Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models.
SAS
Hernán Ponce de León, Florian Furbach, Keijo Heljanko, Roland Meyer
2017 — conf
Structural Feature Selection for Event Logs.
Business Process Management Workshops
Markku Hinkka, Teemu Lehto, Keijo Heljanko, Alexander Jung
2017 J jnl
Structural Feature Selection for Event Logs.
CoRR
Markku Hinkka, Teemu Lehto, Keijo Heljanko, Alexander Jung
2017 B conf
The FMCAD 2017 graduate student forum.
FMCAD
Keijo Heljanko
2017 J jnl
When Do We Not Need Complex Assume-Guarantee Rules?
ACM Trans. Embed. Comput. Syst.
Antti Siirtola, Stavros Tripakis, Keijo Heljanko
2016 C conf
Assessing Big Data SQL Frameworks for Analyzing Event Logs.
PDP
Markku Hinkka, Teemu Lehto, Keijo Heljanko
2016 J jnl
LCTD: Test-guided proofs for C programs on LLVM.
J. Log. Algebraic Methods Program.
Olli Saarikivi, Keijo Heljanko
2016 A conf
LCTD: Tests-Guided Proofs for C Programs on LLVM - (Competition Contribution).
TACAS
Olli Saarikivi, Keijo Heljanko
2016 J jnl
Synchronous counting and computational algorithm design.
J. Comput. Syst. Sci.
Danny Dolev, Keijo Heljanko, Matti Järvisalo, Janne H. Korhonen, Christoph Lenzen, Joel Rybicki, Jukka Suomela, Siert Wieringa
2015 J jnl
Parametrised Modal Interface Automata.
ACM Trans. Embed. Comput. Syst.
Antti Siirtola, Keijo Heljanko
2015 — conf
Reporting Races in Dynamic Partial Order Reduction.
NFM
Olli Saarikivi, Keijo Heljanko
2015 — conf
Unfolding Based Minimal Test Suites for Testing Multithreaded Programs.
ACSD
Hernán Ponce de León, Olli Saarikivi, Kari Kähkönen, Keijo Heljanko, Javier Esparza
2015 J jnl
Unfolding based automated testing of multithreaded programs.
Autom. Softw. Eng.
Kari Kähkönen, Olli Saarikivi, Keijo Heljanko
2015 B conf
Unfolding-Based Process Discovery.
ATVA
Hernán Ponce de León, César Rodríguez, Josep Carmona, Keijo Heljanko, Stefan Haar
2015 J jnl
Unfolding-Based Process Discovery.
CoRR
Hernán Ponce de León, César Rodríguez, Josep Carmona, Keijo Heljanko, Stefan Haar
2015 J jnl
Verifying large modular systems using iterative abstraction refinement.
Reliab. Eng. Syst. Saf.
Jussi Lahtinen, Tuomas Kuismin, Keijo Heljanko
2015 — conf
When Do We (Not) Need Complex Assume-Guarantee Rules?
ACSD
Antti Siirtola, Stavros Tripakis, Keijo Heljanko
2014 J jnl
A symbolic model checking approach to verifying satellite onboard software.
Sci. Comput. Program.
Xiang Gan, Jori Dubrovin, Keijo Heljanko
2014 J jnl
Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks.
J. Satisf. Boolean Model. Comput.
Gianpiero Cabodi, Carmelo Loiacono, Marco Palena, Paolo Pasini, Denis Patti, Stefano Quer, Danilo Vendraminetto, Armin Biere, Keijo Heljanko
2014 — conf
Lightweight State Capturing for Automated Testing of Multithreaded Programs.
TAP@STAF
Kari Kähkönen, Keijo Heljanko
2014 J jnl
SeqPig: simple and scalable scripting for large sequencing data sets in Hadoop.
Bioinform.
André Schumacher, Luca Pireddu, Matti Niemenmaa, Aleksi Kallio, Eija Korpelainen, Gianluigi Zanetti, Keijo Heljanko
2014 — conf
Testing Multithreaded Programs with Contextual Unfoldings and Dynamic Symbolic Execution.
ACSD
Kari Kähkönen, Keijo Heljanko
2013 A conf
Asynchronous Multi-core Incremental SAT Solving.
TACAS
Siert Wieringa, Keijo Heljanko
2013 A conf
Concurrent Clause Strengthening.
SAT
Siert Wieringa, Keijo Heljanko
2013 — conf
Increasing Confidence in Liveness Model Checking Results with Proofs.
Haifa Verification Conference
Tuomas Kuismin, Keijo Heljanko
2013 — conf
Parametrised Compositional Verification with Multiple Process and Data Types.
ACSD
Antti Siirtola, Keijo Heljanko
2013 — ed.
Proceedings the Sixth International Workshop on the Practical Application of Stochastic Modelling, PASM 2012, and the Eleventh International Workshop on Parallel and Distributed Methods in Verification, PDMC 2012, London, UK, September 2012
PASM/PDMC
Jeremy T. Bradley, Keijo Heljanko, William J. Knottenbelt, Nigel Thomas
2012 — ed.
12th International Conference on Application of Concurrency to System Design, ACSD 2012, Hamburg, Germany, June 27-29, 2012
ACSD
Jens Brandt, Keijo Heljanko
2012 J jnl
Exploiting step semantics for efficient bounded model checking of asynchronous systems.
Sci. Comput. Program.
Jori Dubrovin, Tommi A. Junttila, Keijo Heljanko
2012 J jnl
Hadoop-BAM: directly manipulating next generation sequencing data in the cloud.
Bioinform.
Matti Niemenmaa, Aleksi Kallio, André Schumacher, Petri Klemelä, Eija Korpelainen, Keijo Heljanko
2012 — conf
Improving Dynamic Partial Order Reductions for Concolic Testing.
ACSD
Olli Saarikivi, Kari Kähkönen, Keijo Heljanko
2012 J jnl
Model checking of safety-critical software in the nuclear engineering domain.
Reliab. Eng. Syst. Saf.
Jussi Lahtinen, J. Valkonen, Kim Björkman, J. Frits, Ilkka Niemelä, Keijo Heljanko
2012 — conf
Preface.
PASM/PDMC
Jeremy T. Bradley, Keijo Heljanko, William J. Knottenbelt, Nigel Thomas
2012 J jnl
Solving parity games by a reduction to SAT.
J. Comput. Syst. Sci.
Keijo Heljanko, Misa Keinänen, Martin Lange, Ilkka Niemelä
2012 A* conf
Using unfoldings in automated testing of multithreaded programs.
ASE
Kari Kähkönen, Olli Saarikivi, Keijo Heljanko
2011 J jnl
A Symbolic Model Checking Approach to Verifying Satellite Onboard Software.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Xiang Gan, Jori Dubrovin, Keijo Heljanko
2011 J jnl
Efficient model checking of PSL safety properties.
IET Comput. Digit. Tech.
Tuomas Launiainen, Keijo Heljanko, Tommi A. Junttila
2011 — ed.
Proceedings 10th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2011, Snowbird, Utah, USA, July 14, 2011.
PDMC
Jiri Barnat, Keijo Heljanko
2010 — conf
Efficient Model Checking of PSL Safety Properties.
ACSD
Tuomas Launiainen, Keijo Heljanko, Tommi A. Junttila
2010 — conf
Experimental Comparison of Concolic and Random Testing for Java Card Applets.
SPIN
Kari Kähkönen, Roland Kindermann, Keijo Heljanko, Ilkka Niemelä
2009 — conf
Tarmo: A Framework for Parallelized Bounded Model Checking
PDMC
Siert Wieringa, Matti Niemenmaa, Keijo Heljanko
2009 B conf
The LIME Interface Specification Language and Runtime Monitoring Tool.
RV
Kari Kähkönen, Jani Lampinen, Keijo Heljanko, Ilkka Niemelä
2008 — conf
Analyzing Context-Free Grammars Using an Incremental SAT Solver.
ICALP (2)
Roland Axelsson, Keijo Heljanko, Martin Lange
2008 — conf
Symbolic Step Encodings for Object Based Communicating State Machines.
FMOODS
Jori Dubrovin, Tommi A. Junttila, Keijo Heljanko
2008 — book
Unfoldings - A Partial-Order Approach to Model Checking
Javier Esparza, Keijo Heljanko
2006 A* conf
Bounded Model Checking for Weak Alternating Büchi Automata.
CAV
Keijo Heljanko, Tommi A. Junttila, Misa Keinänen, Martin Lange, Timo Latvala
2006 J jnl
Linear Encodings of Bounded LTL Model Checking
CoRR
Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan
2006 J jnl
Linear Encodings of Bounded LTL Model Checking.
Log. Methods Comput. Sci.
Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan
2006 J jnl
Planning as satisfiability: parallel plans and algorithms for plan search.
Artif. Intell.
Jussi Rintanen, Keijo Heljanko, Ilkka Niemelä
2005 J jnl
BMC via on-the-fly determinization.
Int. J. Softw. Tools Technol. Transf.
Toni Jussila, Keijo Heljanko, Ilkka Niemelä
2005 — conf
Complexity Results for Checking Distributed Implementability.
ACSD
Keijo Heljanko, Alin Stefanescu
2005 A* conf
Incremental and Complete Bounded Model Checking for Full PLTL.
CAV
Keijo Heljanko, Tommi A. Junttila, Timo Latvala
2005 B conf
Simple Is Better: Efficient Bounded Model Checking for Past LTL.
VMCAI
Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila
2004 B conf
Parallel Encodings of Classical Planning as Satisfiability.
JELIA
Jussi Rintanen, Keijo Heljanko, Ilkka Niemelä
2004 B conf
Simple Bounded LTL Model Checking.
FMCAD
Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila
2003 — conf
BMC via on-the-fly determinization.
BMC@CAV
Toni Jussila, Keijo Heljanko, Ilkka Niemelä
2003 J jnl
Bounded LTL Model Checking with Stable Models
CoRR
Keijo Heljanko, Ilkka Niemelä
2003 J jnl
Bounded LTL model checking with stable models.
Theory Pract. Log. Program.
Keijo Heljanko, Ilkka Niemelä
2003 — conf
Specification Coverage Aided Test Selection.
ACSD
Tuomo Pyhälä, Keijo Heljanko
2002 — —
Combining symbolic and partial order methods for model checking 1-safe Petri nets.
Keijo Heljanko
2002 A conf
Parallelisation of the Petri Net Unfolding Algorithm.
TACAS
Keijo Heljanko, Victor Khomenko, Maciej Koutny
2002 J jnl
Testing LTL formula translation into Büchi automata.
Int. J. Softw. Tools Technol. Transf.
Heikki Tauriainen, Keijo Heljanko
2001 — conf
Answer Set Programming and Bounded Model Checking.
Answer Set Programming
Keijo Heljanko, Ilkka Niemelä
2001 B conf
Bounded LTL Model Checking with Stable Models.
LPNMR
Keijo Heljanko, Ilkka Niemelä
2001 B conf
Bounded Reachability Checking with Process Semantics.
CONCUR
Keijo Heljanko
2001 — conf
Implementing LTL Model Checking with Net Unfoldings.
SPIN
Javier Esparza, Keijo Heljanko
2000 A* conf
A New Unfolding Approach to LTL Model Checking.
ICALP
Javier Esparza, Keijo Heljanko
2000 J jnl
Coping With Strong Fairness.
Fundam. Informaticae
Timo Latvala, Keijo Heljanko
2000 B conf
Model Checking with Finite Complete Prefixes Is PSPACE-Complete.
CONCUR
Keijo Heljanko
2000 — conf
Testing SPIN's LTL Formula Conversion into Büchi Automata with Randomly Generated Input.
SPIN
Heikki Tauriainen, Keijo Heljanko
1999 A conf
Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets.
TACAS
Keijo Heljanko
1999 J jnl
Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets.
Fundam. Informaticae
Keijo Heljanko
1997 A* conf
prod 3.2: An Advanced Tool for Efficient Reachability Analysis.
CAV
Kimmo Varpaaniemi, Keijo Heljanko, Johan Lilius