| 2026 | CAV | Liveness Proofs for Hardware Model Checking. | Nils Froleyks, Emily Yu, Bart Bogaerts, Armin Biere, Keijo Heljanko |
| 2026 | FM | Certifying Constraints in Hardware Model Checking. | Nils Froleyks, Emily Yu, Armin Biere, Keijo Heljanko |
| 2025 | CAV | Introducing Certificates to the Hardware Model Checking Competition. | Nils Froleyks, Emily Yu, Mathias Preiner, Armin Biere, Keijo Heljanko |
| 2025 | SPIRE | Massively Parallel Computation of Matching Statistics. | Anastasia C. Diseth, Keijo Heljanko, Simon J. Puglisi |
| 2024 | ASPLOS | Towards Unified Analysis of GPU Consistency. | Haining Tong, Natalia Gavrilenko, Hernn Ponce de Len, Keijo Heljanko |
| 2024 | ECAI | Subsystem Discovery in High-Dimensional Time-Series Using Masked Autoencoders. | Teemu Sarapisto, Haoyu Wei, Keijo Heljanko, Arto Klami, Laura Ruotsalainen |
| 2024 | IJCAR | Certifying Phase Abstraction. | Nils Froleyks, Emily Yu, Armin Biere, Keijo Heljanko |
| 2023 | FMCAD | Towards Compositional Hardware Model Checking Certification. | Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko |
| 2022 | FMCAD | Stratified Certification for k-Induction. | Emily Yu, Nils Froleyks, Armin Biere, Keijo Heljanko |
| 2021 | CAV | Progress in Certifying Hardware Model Checking Results. | Emily Yu, Armin Biere, Keijo Heljanko |
| 2020 | TACAS | Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution). | Hernn Ponce de Len, Florian Furbach, Keijo Heljanko, Roland Meyer |
| 2019 | ADBIS | Exploiting Event Log Event Attributes in RNN Based Prediction. | Markku Hinkka, Teemu Lehto, Keijo Heljanko |
| 2019 | CAV | BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. | Natalia Gavrilenko, Hernn Ponce de Len, Florian Furbach, Keijo Heljanko, Roland Meyer |
| 2019 | ICFEM | Certifying Hardware Model Checking Results. | Zhengqi Yu, Armin Biere, Keijo Heljanko |
| 2019 | PERCOM | Access Time Improvement Framework for Standardized IoT Gateways. | Asad Javed, Narges Yousefnezhad, Jrmy Robert, Keijo Heljanko, Kary Frmling |
| 2018 | BPM | Classifying Process Instances Using Recurrent Neural Networks. | Markku Hinkka, Teemu Lehto, Keijo Heljanko, Alexander Jung |
| 2018 | FMCAD | BMC with Memory Models as Modules. | Hernn Ponce de Len, Florian Furbach, Keijo Heljanko, Roland Meyer |
| 2017 | BPM | Structural Feature Selection for Event Logs. | Markku Hinkka, Teemu Lehto, Keijo Heljanko, Alexander Jung |
| 2017 | FMCAD | Hardware model checking competition 2017. | Armin Biere, Tom van Dijk, Keijo Heljanko |
| 2017 | FMCAD | The FMCAD 2017 graduate student forum. | Keijo Heljanko |
| 2017 | SAS | Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models. | Hernn Ponce de Len, Florian Furbach, Keijo Heljanko, Roland Meyer |
| 2016 | PDP | Assessing Big Data SQL Frameworks for Analyzing Event Logs. | Markku Hinkka, Teemu Lehto, Keijo Heljanko |
| 2016 | TACAS | LCTD: Tests-Guided Proofs for C Programs on LLVM - (Competition Contribution). | Olli Saarikivi, Keijo Heljanko |
| 2015 | ATVA | Unfolding-Based Process Discovery. | Hernn Ponce de Len, Csar Rodrguez, Josep Carmona, Keijo Heljanko, Stefan Haar |
| 2014 | TAP | Lightweight State Capturing for Automated Testing of Multithreaded Programs. | Kari Khknen, Keijo Heljanko |
| 2013 | SAT | Concurrent Clause Strengthening. | Siert Wieringa, Keijo Heljanko |
| 2013 | TACAS | Asynchronous Multi-core Incremental SAT Solving. | Siert Wieringa, Keijo Heljanko |
| 2009 | RV | The LIME Interface Specification Language and Runtime Monitoring Tool. | Kari Khknen, Jani Lampinen, Keijo Heljanko, Ilkka Niemel |
| 2008 | ICALP | Analyzing Context-Free Grammars Using an Incremental SAT Solver. | Roland Axelsson, Keijo Heljanko, Martin Lange |
| 2006 | CAV | Bounded Model Checking for Weak Alternating Bchi Automata. | Keijo Heljanko, Tommi A. Junttila, Misa Keinnen, Martin Lange, Timo Latvala |
| 2005 | CAV | Incremental and Complete Bounded Model Checking for Full PLTL. | Keijo Heljanko, Tommi A. Junttila, Timo Latvala |
| 2005 | VMCAI | Simple Is Better: Efficient Bounded Model Checking for Past LTL. | Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila |
| 2004 | FMCAD | Simple Bounded LTL Model Checking. | Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila |
| 2004 | JELIA | Parallel Encodings of Classical Planning as Satisfiability. | Jussi Rintanen, Keijo Heljanko, Ilkka Niemel |
| 2002 | TACAS | Parallelisation of the Petri Net Unfolding Algorithm. | Keijo Heljanko, Victor Khomenko, Maciej Koutny |
| 2001 | CONCUR | Bounded Reachability Checking with Process Semantics. | Keijo Heljanko |
| 2001 | LPNMR | Bounded LTL Model Checking with Stable Models. | Keijo Heljanko, Ilkka Niemel |
| 2000 | CONCUR | Model Checking with Finite Complete Prefixes Is PSPACE-Complete. | Keijo Heljanko |
| 2000 | ICALP | A New Unfolding Approach to LTL Model Checking. | Javier Esparza, Keijo Heljanko |
| 1999 | TACAS | Using Logic Programs with Stable Model Semantics to Solve Deadlock and Reachability Problems for 1-Safe Petri Nets. | Keijo Heljanko |
| 1997 | CAV | prod 3.2: An Advanced Tool for Efficient Reachability Analysis. | Kimmo Varpaaniemi, Keijo Heljanko, Johan Lilius |