to appear |
|
75 | Kari Kähkönen, Olli Saarikivi, and Keijo Heljanko. LCT: A parallel distributed testing tool for multithreaded Java programs. In Proceedings of the 11th International Workshop on Parallel and Distributed Methods in verifiCation ( PDMC 2012), to appear. |
|
2013 |
|
74 | Siert Wieringa and Keijo Heljanko. Asynchronous multi-core incremental sat solving. In Nir Piterman and Scott A. Smolka, editors, Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), volume 7795 of Lecture Notes in Computer Science, pages 139–153, 2013. |
|
2012 |
|
73 | Jens Brandt and Keijo Heljanko. Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD 2012). IEEE, Hamburg, Germany, 2012. |
|
|
72 | Kari Kähkönen, Olli Saarikivi, and Keijo Heljanko. Using unfoldings in automated testing of multithreaded programs. In Proceedings of the 27th IEEE/ACM International Conference Automated Software Engineering 2012 (ASE 2012), pages 150–159, 2012. |
|
|
71 | Jussi Lahtinen, Janne Valkonen, Kim Björkman, Juho Frits, Ilkka Niemelä, and Keijo Heljanko. Model checking of safety-critical software in the nuclear engineering domain. Reliability Engineering & System Safety (RESS), 105(0):104–113, 2012. |
|
|
70 | Jussi Lahtinen, Tuomas Launiainen, Keijo Heljanko, and Jonatan Ropponen. Model checking methodology for large systems, faults and asynchronous behaviour - SARANA 2011 work report. VTT Technology 12, VTT Technical Research Centre of Finland, Espoo, 2012. |
|
|
69 | Olli Saarikivi, Kari Kähkönen, and Keijo Heljanko. Improving dynamic partial order reductions for concolic testing. In Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD 2012), pages 132–141, 2012. |
|
|
68 | Matti Niemenmaa, Aleksi Kallio, André Schumacher, Petri Klemelä, Eija Korpelainen, and Keijo Heljanko. Hadoop-BAM: Directly manipulating next generation sequencing data in the cloud. Bioinformatics, 28(6):876–877, 2012. |
|
|
67 | Xiang Gan, Jori Dubrovin, and Keijo Heljanko. A symbolic model checking approach to verifying satellite onboard software. Electronic Communications of the EASST - Proceedings of the 11th International Workshop on Automated Verification of Critical Systems (AVOCS 2011), 46(0):1–15, 2012. |
|
|
66 | Keijo Heljanko, Misa Keinänen, Martin Lange, and Ilkka Niemelä. Solving parity games by a reduction to SAT. Journal of Computer and System Sciences, 78(2):430–440, 2012. |
|
|
65 | Jori Dubrovin, Tommi Junttila, and Keijo Heljanko. Exploiting step semantics for efficient bounded model checking of asynchronous systems. Science of Computer Programming, 77(10–11):1095–1121, 2012. |
|
2011 |
|
64 | Kari Kähkönen, Tuomas Launiainen, Olli Saarikivi, Janne Kauttio, Keijo Heljanko, and Ilkka Niemelä. LCT: An open source concolic testing tool for Java programs. In Proceedings of the 6th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE'2011), pages 75–80, Saarbrücken, Germany, Mar 2011. |
|
|
63 | Matti Niemenmaa, André Schumacher, Keijo Heljanko, Aleksi Kallio, Petri Klemelä, Taavi Hupponen, and Eija Korpelainen. Hadoop-BAM: A library for genomic data processing. In Proceedings of the 12th Annual Bioinformatics Open Source Conference (BOSC 2011), page 1, 2011. Available online at http://www.oboedit.org/BOSC2011/BOSC2011-program.pdf. |
|
|
62 | Jiri Barnat and Keijo Heljanko. Proceedings of the 10th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2011), volume 72 of Electronic Proceedings in Theoretical Computer Science. Electronic Proceedings in Theoretical Computer Science, 2011. |
|
|
61 | Tuomas Launiainen, Keijo Heljanko, and Tommi Junttila. Efficient model checking of PSL safety properties. IET Computers & Digital Techniques, 5(6):479–492, 2011. |
|
2010 |
|
60 | Tuomas Launiainen, Keijo Heljanko, and Tommi Junttila. Efficient model checking of PSL safety properties. In Proceedings of the 10th International Conference on Application of Concurrency to System Design (ACSD'2010), pages 95–104, Braga, Portugal, June 2010. |
|
|
59 | Kari Kähkönen, Roland Kindermann, Keijo Heljanko, and Ilkka Niemelä. Experimental comparison of concolic and random testing for Java Card applets. In Jaco van de Pol and Michael Weber, editors, SPIN, volume 6349 of Lecture Notes in Computer Science, pages 22–39, 2010. |
|
2009 |
|
58 | Jani Lampinen, Sami Liedes, Kari Kähkönen, Janne Kauttio, and Keijo Heljanko. Interface specification methods for software components. Technical Report TKK-ICS-R25, Helsinki University of Technology, Department of Information and Computer Science, Espoo, Finland, December 2009. |
|
|
57 | Kim Björkman, Juho Frits, Janne Valkonen, Jussi Lahtinen, Keijo Heljanko, Ilkka Niemelä, and Jari J. Hämäläinen. Verification of safety logic designs by model checking. In Proceedings of the Sixth American Nuclear Society International Topical Meeting on Nuclear Plant Instrumentation, Control, and Human-Machine Interface Technologies NPIC&HMIT 2009, Knoxville, Tennessee, April 2009. |
|
|
56 | Siert Wieringa, Matti Niemenmaa, and Keijo Heljanko. Tarmo: A framework for parallelized bounded model checking. In Lubos Brim and Jaco van der Pol, editors, Proceedings of the 8th International Workshop on Parallel and Distributed Methods in Verification (PDMC'09), volume 14 of Electronic Proceedings in Theoretical Computer Science (EPTCS), pages 62–76, 2009. |
|
|
55 | Kim Björkmann, Juho Frits, Janne Valkonen, Keijo Heljanko, and Ilkka Niemelä. Model-based analysis of a stepwise shutdown logic. VTT Working Papers 115, VTT Technical Research Centre of Finland, Espoo, 2009. |
|
|
54 | Janne Valkonen, Matti Koskimies, Kim Björkman, Keijo Heljanko, Ilkka Niemelä, and Jari J. Hämäläinen. Formal verification of safety automation logic designs. In Automaatio XVIII 2009 Seminaari, pages 1–1, 2009. |
|
|
53 | Kari Kähkönen, Jani Lampinen, Keijo Heljanko, and Ilkka Niemelä. The LIME interface specification language and runtime monitoring tool. In Saddek Bensalem and Doron Peled, editors, Proceedings of the 9th International Workshop on Runtime Verification (RV'09), volume 5779 of Lecture Notes in Computer Science, pages 93–100, 2009. |
|
2008 |
|
52 | Roland Axelsson, Keijo Heljanko, and Martin Lange. Analyzing context-free grammars using an incremental SAT solver. In Luca Aceto, Ivan Damgård, Leslie Ann Goldberg, Magnús M. Halldórsson, Anna Ingólfsdóttir, and Igor Walukiewicz, editors, Proceedings of the 35th International Colloquium on Automata, Languages, and Programming (ICALP'08), Part II, volume 5126 of Lecture Notes in Computer Science, pages 410–422, Reykjavik, Iceland, July 2008. Springer-Verlag. |
|
|
51 | Jori Dubrovin, Tommi Junttila, and Keijo Heljanko. Symbolic step encodings for object based communicating state machines. In Gilles Barthe and Frank S. de Boer, editors, Proceedings of the 10th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), volume 5051 of Lecture Notes in Computer Science, pages 96–112, Oslo, Norway, June 2008. Springer-Verlag. |
|
|
50 | Janne Valkonen, Matti Koskimies, Ville Pettersson, Keijo Heljanko, Jan-Erik Holmberg, Ilkka Niemelä, and Jari J. Hämäläinen. Formal verification of safety I&C system designs: Two nuclear power plant related applications. In Enlarged Halden Programme Group Meeting – Proceedings of the Man-Technology-Organisation Sessions, page C4.2, Loen, Norway, May 2008. Institutt for Energiteknikk, Halden, Norway. |
|
|
49 | Janne Valkonen, Ilkka Karanta, Matti Koskimies, Keijo Heljanko, Ilkka Niemelä, Dan Sheridan, and Robin E. Bloomfield. NPP safety automation systems analysis – State of the art. VTT Working Papers 94, VTT Technical Research Centre of Finland, Espoo, Finland, April 2008. |
|
|
48 | Javier Esparza and Keijo Heljanko. Unfoldings – A Partial-Order Approach to Model Checking. EATCS Monographs in Theoretical Computer Science. Springer-Verlag, March 2008. |
|
|
47 | Janne Valkonen, Ville Petterson, Kim Björkman, Jan-Erik Holmberg, Matti Koskimies, Keijo Heljanko, and Ilkka Niemelä. Model-based analysis of an arc protection and an emergency cooling system – MODSAFE 2007 working report. VTT Working Papers 93, VTT Technical Research Centre of Finland, Espoo, Finland, February 2008. |
|
2007 |
|
46 | Jori Dubrovin, Tommi Junttila, and Keijo Heljanko. Symbolic step encodings for object based communicating state machines. Technical Report B24, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2007. |
|
2006 |
|
45 | Keijo Heljanko, Tommi Junttila, Misa Keinänen, Martin Lange, and Timo Latvala. Bounded model checking for weak alternating Büchi automata. In Thomas Ball and Robert B. Jones, editors, Proceedings of the 18th International Conference on Computer Aided Verification (CAV'2006), volume 4144 of Lecture Notes in Computer Science, pages 95–108, Seattle, WA, USA, August 2006. Springer-Verlag. |
|
|
44 | Armin Biere, Keijo Heljanko, Tommi Junttila, Timo Latvala, and Viktor Schuppan. Linear encodings of bounded LTL model checking. Logical Methods in Computer Science, 2(5:5), 2006. (doi: 10.2168/LMCS-2(5:5)2006). |
|
|
43 | Jussi Rintanen, Keijo Heljanko, and Ilkka Niemelä. Planning as satisfiability: parallel plans and algorithms for plan search. Artificial Intelligence, 170(12-13):1031–1080, 2006. |
|
2005 |
|
42 | Keijo Heljanko, Tommi Junttila, and Timo Latvala. Incremental and complete bounded model checking for full PLTL. In Kousha Etessami and Sriram K. Rajamani, editors, Proceedings of the 17th International Conference on Computer Aided Verification (CAV'2005), volume 3576 of Lecture Notes in Computer Science, pages 98–111, Edinburgh, Scotland, United Kingdom, July 2005. Springer-Verlag. |
|
|
41 | Keijo Heljanko and Alin Stefanescu. Complexity results for checking distributed implementability. In Jörg Desel and Yosinori Watanabe, editors, Proceedings of the 5th International Conference on Application of Concurrency to System Design (ACSD'2005), pages 78–87, St Malo, France, June 2005. IEEE Computer Society. |
|
|
40 | Jussi Rintanen, Keijo Heljanko, and Ilkka Niemelä. Planning as satisfiability: Parallel plans and algorithms for plan search. Technical Report 216, Institute of Computer Science, University of Freiburg, Freiburg, Germany, 2005. |
|
|
39 | Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. Simple is better: Efficient bounded model checking for past LTL. In Radia Cousot, editor, Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'2005), volume 3385 of Lecture Notes in Computer Science, pages 380–395, Paris, France, January 2005. Springer-Verlag. |
|
|
38 | Toni Jussila, Keijo Heljanko, and Ilkka Niemelä. BMC via on-the-fly determinization. STTT - International Journal on Software Tools for Technology Transfer, 7(2):89–101, 2005. |
|
2004 |
|
37 | Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. Simple bounded LTL model checking. In Alan Hu and Andy Martin, editors, Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04), volume 3312 of Lecture Notes in Computer Science, pages 186–200. Springer-Verlag, November 2004. |
|
|
36 | Keijo Heljanko and Alin Stefanescu. Complexity results for checking distributed implementability. Technical Report 05/2004, Institute of Formal Methods in Computer Science, University of Stuttgart, Stuttgart, Germany, October 2004. |
|
|
35 | Jussi Rintanen, Keijo Heljanko, and Ilkka Niemelä. Parallel encodings of classical planning as satisfiability. In José Júlio Alferes and João Alexandre Leite, editors, Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA'04), volume 3229 of Lecture Notes in Computer Science, pages 307–319, Lisbon, Portugal, September 2004. Springer-Verlag. |
|
|
34 | Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. Simple bounded LTL model checking. Research Report A92, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, July 2004. |
|
|
33 | Jussi Rintanen, Keijo Heljanko, and Ilkka Niemelä. Parallel encodings of classical planning as satisfiability. Technical Report 198, Institute of Computer Science, University of Freiburg, Freiburg, Germany, February 2004. |
|
2003 |
|
32 | Toni Jussila, Keijo Heljanko, and Ilkka Niemelä. BMC via on-the-fly determinization. In Ofer Strichman and Armin Biere, editors, Electronic Notes in Theoretical Computer Science, volume 89, pages 561–577. Elsevier, July 2003. |
|
|
31 | Tuomo Pyhälä and Keijo Heljanko. Specification coverage aided test selection. In Johan Lilius, Felice Balarin, and Ricardo J. Machado, editors, Proceeding of the 3rd International Conference on Application of Concurrency to System Design (ACSD'2003), pages 187–195, Guimaraes, Portugal, June 2003. IEEE Computer Society. |
|
|
30 | Tuomo Pyhälä and Keijo Heljanko. Bomotest: A formal conformance testing tool, version 1.5. Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, 2003. Software. |
|
|
29 | Keijo Heljanko and Ilkka Niemelä. Bounded LTL model checking with stable models. Theory and Practice of Logic Programming, 3(4&5):519–550, 2003. Also available as (CoRR: arXiv:cs.LO/0305040). |
|
2002 |
|
28 | Keijo Heljanko, Victor Khomenko, and Maciej Koutny. Parallelisation of the Petri net unfolding algorithm. In Joost-Pieter Katoen and Perdita Stevens, editors, Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'2002), volume 2280 of Lecture Notes in Computer Science, pages 371–385, Grenoble, France, April 2002. Springer-Verlag. |
|
|
27 | Keijo Heljanko. Combining Symbolic and Partial Order Methods for Model Checking 1-Safe Petri Nets. PhD thesis, Helsinki University of Technology, Department of Computer Science and Engineering, Espoo, Finland, February 2002. Also available as: Series A: Research Report 71, Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science. |
|
|
26 | Heikki Tauriainen and Keijo Heljanko. Testing LTL formula translation into Büchi automata. STTT - International Journal on Software Tools for Technology Transfer, 4(1):57–70, 2002. |
|
2001 |
|
25 | Keijo Heljanko and Ilkka Niemelä. Bounded LTL model checking with stable models. In Thomas Eiter, Wolfgang Faber, and Mirosaw Truszczynski, editors, Proceedings of the 6th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'2001), volume 2173 of Lecture Notes in Artificial Intelligence, pages 200–212, Vienna, Austria, September 2001. Springer-Verlag. |
|
|
24 | Keijo Heljanko. Bounded reachability checking with process semantics. In Kim Guldstrand Larsen and Mogens Nielsen, editors, Proceedings of the 12th International Conference on Concurrency Theory (Concur'2001), volume 2154 of Lecture Notes in Computer Science, pages 218–232, Aalborg, Denmark, August 2001. Springer-Verlag. |
|
|
23 | Keijo Heljanko, Victor Khomenko, and Maciej Koutny. Parallelisation of the Petri net unfolding algorithm. Technical Report CS-TR-733, Department of Computer Science, University of Newcastle upon Tyne, Newcastle, United Kindom, June 2001. |
|
|
22 | Javier Esparza and Keijo Heljanko. Implementing LTL model checking with net unfoldings. In Matthew B. Dwyer, editor, Proceedings of the 8th International SPIN Workshop on Model Checking of Software (SPIN'2001), volume 2057 of Lecture Notes in Computer Science, pages 37–56, Toronto, Canada, May 2001. Springer-Verlag. |
|
|
21 | Javier Esparza and Keijo Heljanko. Implementing LTL model checking with net unfoldings. Series A: Research Report 68, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, March 2001. |
|
|
20 | Keijo Heljanko and Ilkka Niemelä. Answer set programming and bounded model checking. In Alessandro Provetti and Tran Cao Son, editors, Proceedings of the AAAI Spring 2001 Symposium on Answer Set Programming: Towards Efficient and Scalable Knowledge Representation and Reasoning, pages 90–96, Stanford, USA, March 2001. AAAI Press, Technical Report SS-01-01. |
|
|
19 | Keijo Heljanko. punroll 0.3: a bounded reachability checker. Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, 2001. Software. |
|
|
18 | Keijo Heljanko and Patrik Simons. boundsmodels 0.9: a bounded LTL model checker. Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, 2001. Software. |
|
|
17 | Keijo Heljanko and Patrik Simons. unfsmodels 0.9: a LTL model checker using net unfoldings. Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, 2001. Software. |
|
2000 |
|
16 | Keijo Heljanko and Ilkka Niemelä. Petri net analysis and nonmonotonic reasoning. In Nisse Husberg, Tomi Janhunen, and Ilkka Niemelä, editors, Leksa Notes in Computer Science - Festschrift in Honour of Professor Leo Ojala, pages 7–19, Espoo, Finland, October 2000. Helsinki University of Technology, Laboratory for Theoretical Computer Science. |
|
|
15 | Heikki Tauriainen and Keijo Heljanko. Testing SPIN's LTL formula conversion into Büchi automata with randomly generated input. In Klaus Havelund, John Penix, and Willem Visser, editors, Proceedings of the 7th International SPIN Workshop on Model Checking of Software (SPIN'2000), volume 1885 of Lecture Notes in Computer Science, pages 54–72, Stanford University, California, USA, August 2000. Springer-Verlag. |
|
|
14 | Keijo Heljanko. Model checking with finite complete prefixes is PSPACE-complete. In Catuscia Palamidessi, editor, Proceedings of the 11th International Conference on Concurrency Theory (Concur'2000), volume 1877 of Lecture Notes in Computer Science, pages 108–122, State College, Pennsylvania, USA, August 2000. Springer-Verlag. |
|
|
13 | Javier Esparza and Keijo Heljanko. A new unfolding approach to LTL model checking. In Ugo Montanari, José D. P. Rolim, and Emo Welzl, editors, Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP'2000), volume 1853 of Lecture Notes in Computer Science, pages 475–486, Geneva, Switzerland, July 2000. Springer-Verlag. |
|
|
12 | Javier Esparza and Keijo Heljanko. A new unfolding approach to LTL model checking. Series A: Research Report 60, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, April 2000. |
|
|
11 | Timo Latvala and Keijo Heljanko. Coping with strong fairness. Fundamenta Informaticae, 43(1–4):175–193, 2000. |
|
1999 |
|
10 | Keijo Heljanko. Deadlock and Reachability Checking with Finite Complete Prefixes. Licentiate's thesis, Helsinki University of Technology, Department of Computer Science and Engineering, Espoo, Finland, December 1999. Also available as: Series A: Research Report 56, Helsinki University of Technology, Department of Computer Science and Engineering, Laboratory for Theoretical Computer Science. |
|
|
9 | Timo Latvala and Keijo Heljanko. Coping with strong fairness – on-the-fly emptiness checking for Streett automata. In H.-D. Burkhard, L. Czaja, H.-S. Nguyen, and P. Starke, editors, Proceedings of the Workshop Concurrency, Specification & Programming 1999, pages 107–118, Warsaw, Poland, September 1999. Warsaw University. |
|
|
8 | Keijo Heljanko. Minimizing finite complete prefixes. In H.-D. Burkhard, L. Czaja, H.-S. Nguyen, and P. Starke, editors, Proceedings of the Workshop Concurrency, Specification & Programming 1999, pages 83–95, Warsaw, Poland, September 1999. Warsaw University. |
|
|
7 | Keijo Heljanko and Patrik Simons. mcsmodels 1.4: a deadlock and reachability checker using net unfoldings. Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, 1999. Software. |
|
|
6 | Keijo Heljanko. Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets. Fundamenta Informaticae, 37(3):247–268, 1999. |
|
|
5 | Keijo Heljanko. Using logic programs with stable model semantics to solve deadlock and reachability problems for 1-safe Petri nets. In Rance Cleaveland, editor, Proceedings of 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), volume 1579 of Lecture Notes in Computer Science, pages 240–254, Amsterdam, Netherlands, 1999. Springer-Verlag. |
|
1998 |
|
4 | Keijo Heljanko. Deadlock checking for complete finite prefixes using logic programs with stable model semantics (Extended abstract). In H.-D. Burkhard, L. Czaja, and P. Starke, editors, Proceedings of the Workshop Concurrency, Specification & Programming 1998, Informatik-Bericht Nr. 110, pages 106–115, Berlin, Germany, September 1998. Humboldt-University, Berlin. |
|
1997 |
|
3 | Kimmo Varpaaniemi, Keijo Heljanko, and Johan Lilius. PROD 3.2 - An advanced tool for efficient reachability analysis. In Orna Grumberg, editor, Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97), volume 1254 of Lecture Notes in Computer Science, pages 472–475, Haifa, Israel, June 1997. Springer-Verlag. |
|
|
2 | Keijo Heljanko. Model checking the branching time temporal logic CTL. Master's thesis, Helsinki University of Technology, Department of Computer Science and Engineering, Espoo, Finland, May 1997. Also available as: Series A: Research Report 45, Helsinki University of Technology, Department of Computer Science and Engineering, Digital Systems Laboratory. |
|
1996 |
|
1 | Keijo Heljanko. Implementing a CTL model checker. In L. Czaja, P. Starke, H.-D. Burkhard, and M. Lenz, editors, Proceedings of the Workshop Concurrency, Specification & Programming 1996, Informatik-Bericht Nr. 69, pages 75–84, Berlin, Germany, September 1996. Humboldt-University, Berlin. |
|
