Keijo Heljanko

Proceedings of the Computer Aided Verification - 33rd International Conference, 2021

2020

An optimal cut-off algorithm for parameterised refinement checking.

[BibT_eX]

[DOI]

Sci. Comput. Program., 2020

IoTEF: A Federated Edge-Cloud Architecture for Fault-Tolerant IoT Applications.

[BibT_eX]

[DOI]

J. Grid Comput., 2020

Reinforcement learning of adaptive online rescheduling timing and computing time allocation.

[BibT_eX]

[DOI]

Teemu J. Ikonen

Iiro Harjunkoski

Comput. Chem. Eng., 2020

Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2020

Scalable Reference Genome Assembly from Compressed Pan-Genome Index with Spark.

[BibT_eX]

[DOI]

Proceedings of the Big Data - BigData 2020, 2020

2019

Exploiting Event Log Data-Attributes in RNN Based Prediction.

[BibT_eX]

[DOI]

Markku Hinkka

Teemu Lehto

CoRR, 2019

Access Time Improvement Framework for Standardized IoT Gateways.

[BibT_eX]

[DOI]

Proceedings of the IEEE International Conference on Pervasive Computing and Communications Workshops, 2019

Certifying Hardware Model Checking Results.

[BibT_eX]

[DOI]

Zhengqi Yu

Armin Biere

Proceedings of the Formal Methods and Software Engineering, 2019

BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 31st International Conference, 2019

Exploiting Event Log Event Attributes in RNN Based Prediction.

[BibT_eX]

[DOI]

Markku Hinkka

Teemu Lehto

Proceedings of the New Trends in Databases and Information Systems, 2019

2018

Testing Programs with Contextual Unfoldings.

[BibT_eX]

[DOI]

ACM Trans. Embed. Comput. Syst., 2018

ViraPipe: scalable parallel pipeline for viral metagenome analysis from next generation sequencing reads.

[BibT_eX]

[DOI]

Bioinform., 2018

CEFIoT: A fault-tolerant IoT architecture for edge and cloud.

[BibT_eX]

[DOI]

Proceedings of the 4th IEEE World Forum on Internet of Things, 2018

BMC with Memory Models as Modules.

[BibT_eX]

[DOI]

Proceedings of the 2018 Formal Methods in Computer Aided Design, 2018

Dynamic Cut-Off Algorithm for Parameterised Refinement Checking.

[BibT_eX]

[DOI]

Proceedings of the Formal Aspects of Component Software - 15th International Conference, 2018

Classifying Process Instances Using Recurrent Neural Networks.

[BibT_eX]

[DOI]

Proceedings of the Business Process Management Workshops, 2018

2017

When Do We Not Need Complex Assume-Guarantee Rules?

[BibT_eX]

[DOI]

Stavros Tripakis

ACM Trans. Embed. Comput. Syst., 2017

Minimizing Test Suites with Unfoldings of Multithreaded Programs.

[BibT_eX]

[DOI]

ACM Trans. Embed. Comput. Syst., 2017

Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all Models.

[BibT_eX]

[DOI]

CoRR, 2017

Portability Analysis for Weak Memory Models. PORTHOS: One Tool for all Models.

[BibT_eX]

[DOI]

Proceedings of the Static Analysis - 24th International Symposium, 2017

The FMCAD 2017 graduate student forum.

[BibT_eX]

[DOI]

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

Hardware model checking competition 2017.

[BibT_eX]

[DOI]

Armin Biere

Tom van Dijk

Proceedings of the 2017 Formal Methods in Computer Aided Design, 2017

Structural Feature Selection for Event Logs.

[BibT_eX]

[DOI]

Proceedings of the Business Process Management Workshops, 2017

2016

LCTD: Test-guided proofs for C programs on LLVM.

[BibT_eX]

[DOI]

J. Log. Algebraic Methods Program., 2016

Synchronous counting and computational algorithm design.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2016

LCTD: Tests-Guided Proofs for C Programs on LLVM - (Competition Contribution).

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2016

Assessing Big Data SQL Frameworks for Analyzing Event Logs.

[BibT_eX]

[DOI]

Markku Hinkka

Teemu Lehto

Proceedings of the 24th Euromicro International Conference on Parallel, 2016

2015

Parametrised Modal Interface Automata.

[BibT_eX]

[DOI]

ACM Trans. Embed. Comput. Syst., 2015

Verifying large modular systems using iterative abstraction refinement.

[BibT_eX]

[DOI]

Jussi Lahtinen

Tuomas Kuismin

Reliab. Eng. Syst. Saf., 2015

Unfolding based automated testing of multithreaded programs.

[BibT_eX]

[DOI]

Autom. Softw. Eng., 2015

Reporting Races in Dynamic Partial Order Reduction.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 7th International Symposium, 2015

Unfolding-Based Process Discovery.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2015

Unfolding Based Minimal Test Suites for Testing Multithreaded Programs.

[BibT_eX]

[DOI]

Proceedings of the 15th International Conference on Application of Concurrency to System Design, 2015

2014

A symbolic model checking approach to verifying satellite onboard software.

[BibT_eX]

[DOI]

Xiang Gan

Jori Dubrovin

Sci. Comput. Program., 2014

Hardware Model Checking Competition 2014: An Analysis and Comparison of Solvers and Benchmarks.

[BibT_eX]

[DOI]

J. Satisf. Boolean Model. Comput., 2014

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

[BibT_eX]

[DOI]

Bioinform., 2014

Lightweight State Capturing for Automated Testing of Multithreaded Programs.

[BibT_eX]

[DOI]

Proceedings of the Tests and Proofs - 8th International Conference, 2014

Testing Multithreaded Programs with Contextual Unfoldings and Dynamic Symbolic Execution.

[BibT_eX]

[DOI]

Proceedings of the 14th International Conference on Application of Concurrency to System Design, 2014

2013

Asynchronous Multi-core Incremental SAT Solving.

[BibT_eX]

[DOI]

Siert Wieringa

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2013

Concurrent Clause Strengthening.

[BibT_eX]

[DOI]

Siert Wieringa

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2013, 2013

Increasing Confidence in Liveness Model Checking Results with Proofs.

[BibT_eX]

[DOI]

Tuomas Kuismin

Proceedings of the Hardware and Software: Verification and Testing, 2013

Parametrised Compositional Verification with Multiple Process and Data Types.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Application of Concurrency to System Design, 2013

2012

Exploiting step semantics for efficient bounded model checking of asynchronous systems.

[BibT_eX]

[DOI]

Jori Dubrovin

Sci. Comput. Program., 2012

Model checking of safety-critical software in the nuclear engineering domain.

[BibT_eX]

[DOI]

Reliab. Eng. Syst. Saf., 2012

Solving parity games by a reduction to SAT.

[BibT_eX]

[DOI]

J. Comput. Syst. Sci., 2012

Preface.

[BibT_eX]

[DOI]

Jeremy T. Bradley

William J. Knottenbelt

Nigel Thomas

Proceedings of the Proceedings the Sixth International Workshop on the Practical Application of Stochastic Modelling, 2012

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

[BibT_eX]

[DOI]

Bioinform., 2012

Using unfoldings in automated testing of multithreaded programs.

[BibT_eX]

[DOI]

Proceedings of the IEEE/ACM International Conference on Automated Software Engineering, 2012

Improving Dynamic Partial Order Reductions for Concolic Testing.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Application of Concurrency to System Design, 2012

2011

Efficient model checking of PSL safety properties.

[BibT_eX]

[DOI]

Tuomas Launiainen

IET Comput. Digit. Tech., 2011

2010

Experimental Comparison of Concolic and Random Testing for Java Card Applets.

[BibT_eX]

[DOI]

Proceedings of the Model Checking Software, 2010

2009

Tarmo: A Framework for Parallelized Bounded Model Checking

[BibT_eX]

[DOI]

Siert Wieringa

Matti Niemenmaa

Proceedings of the Proceedings 8th International Workshop on Parallel and Distributed Methods in verifiCation, 2009

The LIME Interface Specification Language and Runtime Monitoring Tool.

[BibT_eX]

[DOI]

Proceedings of the Runtime Verification, 9th International Workshop, 2009

2008

Unfoldings - A Partial-Order Approach to Model Checking

[BibT_eX]

[DOI]

Javier Esparza

Monographs in Theoretical Computer Science. An EATCS Series, Springer, ISBN: 978-3-540-77426-6, 2008

Analyzing Context-Free Grammars Using an Incremental SAT Solver.

[BibT_eX]

[DOI]

Roland Axelsson

Martin Lange

Proceedings of the Automata, Languages and Programming, 35th International Colloquium, 2008

Symbolic Step Encodings for Object Based Communicating State Machines.

[BibT_eX]

[DOI]

Jori Dubrovin

Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2008

2006

Linear Encodings of Bounded LTL Model Checking.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2006

Planning as satisfiability: parallel plans and algorithms for plan search.

[BibT_eX]

[DOI]

Jussi Rintanen

Artif. Intell., 2006

Bounded Model Checking for Weak Alternating Büchi Automata.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

BMC via on-the-fly determinization.

[BibT_eX]

[DOI]

Toni Jussila

Int. J. Softw. Tools Technol. Transf., 2005

Simple Is Better: Efficient Bounded Model Checking for Past LTL.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2005

Incremental and Complete Bounded Model Checking for Full PLTL.

[BibT_eX]

[DOI]

Timo Latvala

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

Complexity Results for Checking Distributed Implementability.

[BibT_eX]

[DOI]

Alin Stefanescu

Proceedings of the Fifth International Conference on Application of Concurrency to System Design (ACSD 2005), 2005

2004

Parallel Encodings of Classical Planning as Satisfiability.

[BibT_eX]

[DOI]

Jussi Rintanen

Proceedings of the Logics in Artificial Intelligence, 9th European Conference, 2004

Simple Bounded LTL Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods in Computer-Aided Design, 5th International Conference, 2004

2003

Bounded LTL model checking with stable models.

[BibT_eX]

[DOI]

Theory Pract. Log. Program., 2003

Specification Coverage Aided Test Selection.

[BibT_eX]

[DOI]

Tuomo Pyhälä

Proceedings of the 3rd International Conference on Application of Concurrency to System Design (ACSD 2003), 2003

2002

Combining symbolic and partial order methods for model checking 1-safe Petri nets.

[BibT_eX]

[DOI]

PhD thesis, 2002

Testing LTL formula translation into Büchi automata.

[BibT_eX]

[DOI]

Heikki Tauriainen

Int. J. Softw. Tools Technol. Transf., 2002

Parallelisation of the Petri Net Unfolding Algorithm.

[BibT_eX]

[DOI]

Victor Khomenko

Maciej Koutny

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2002

2001

Implementing LTL Model Checking with Net Unfoldings.

[BibT_eX]

[DOI]

Javier Esparza

Proceedings of the Model Checking Software, 2001

Bounded Reachability Checking with Process Semantics.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2001, 2001

Answer Set Programming and Bounded Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Answer Set Programming, 2001

2000

Coping With Strong Fairness.

[BibT_eX]

[DOI]

Timo Latvala

Fundam. Informaticae, 2000

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

[BibT_eX]

[DOI]

Heikki Tauriainen

Proceedings of the SPIN Model Checking and Software Verification, 7th International SPIN Workshop, Stanford, CA, USA, August 30, 2000

A New Unfolding Approach to LTL Model Checking.

[BibT_eX]

[DOI]

Javier Esparza

Proceedings of the Automata, Languages and Programming, 27th International Colloquium, 2000

Model Checking with Finite Complete Prefixes Is PSPACE-Complete.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2000, 2000

1999

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

[BibT_eX]

[DOI]

Fundam. Informaticae, 1999

1997

prod 3.2: An Advanced Tool for Efficient Reachability Analysis.

[BibT_eX]

[DOI]

Kimmo Varpaaniemi