Book chapters

• Rolf Drechsler, Tommi Junttila, Ilkka Niemelä. Non-Clausal SAT and ATPG. Chapter 21 in Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, IOS Press, 2009. [bibtex entry]

• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz, and Roberto Sebastiani. MathSAT: Tight integration of SAT and mathematical decision procedures. In SAT 2005; Satisfiability Research in the Year 2005, pages 265-293, Springer, 2006. [Bibtex Entry] This is a reprint of the same article in the number 1-3 of volume 25 of the Journal of Automated Reasoning, 2005.

Journal papers

• 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, September 2012. [bibtex entry].

• Tuomas Launiainen, Keijo Heljanko, and Tommi Junttila. Efficient model checking of PSL safety properties. IET Computers and Digital Techniques 5(6):479-492, November 2011. [bibtex entry].

• Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Partitioning Search Spaces of a Randomized Search. Fundamenta Informatica 107(2-3):289-311, 2011. [bibtex entry].

• Antti E. J. Hyvärinen, Tommi Junttila, Ilkka Niemelä. Incorporating Clause Learning in Grid-Based Randomized SAT Solving. Journal on Satisfiability, Boolean Modeling and Computation 6:223-244, 2009. [bibtex entry]

• Matti Järvisalo and Tommi Junttila. Limitations of Restricted Branching in Clause Learning. Constraints 14(3):325-356, 2009. [bibtex entry]

• 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):1-64, 2006. [Bibtex Entry] [PDF]

• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Silvio Ranise, Peter van Rossum, and Roberto Sebastiani. Efficient theory combination via Boolean search. Information and Computation, 204(10):1493-1525, 2006. [Bibtex Entry]

• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz, and Roberto Sebastiani. MathSAT: Tight integration of SAT and mathematical decision procedures. Journal of Automated Reasoning, 35(1-3):265-293, 2005. [Bibtex Entry]

• Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. Unrestricted vs restricted cut in a tableau method for Boolean circuits. Annals of Mathematics and Artificial Intelligence, 44(4):373-399, August 2005. [Bibtex Entry]

• Tommi A. Junttila. Computational Complexity of the Place/Transition-Net Symmetry Reduction Method. Journal of Universal Computer Science, 7(4):307-326, 2001. [Bibtex Entry]

• Tommi A. Junttila. Finding symmetries of algebraic system nets. Fundamenta Informaticae, 37(3):269-289, February 1999. [Gzipped postscript] [Bibtex Entry]

Conference papers

• Tero Laitinen, Tommi Junttila, and Ilkka Niemelä. Simulating Parity Reasoning. In LPAR 2013, pages 568-583, Springer, 2013. [bibtex entry]. [Full version with proofs].

• Roland Kindermann, Tommi Junttila, and Ilkka Niemelä. Bounded Model Checking of an MITL Fragment for Timed Automata. In ACSD 2013, pages 216--225, IEEE, 2013. [bibtex entry]. [Full version with proofs].

• Tero Laitinen, Tommi Junttila, and Ilkka Niemelä. Extending Clause Learning SAT Solvers with Complete Parity Reasoning. In ICTAI 2012, pages 65-72, IEEE, 2012. [bibtex entry]. [Full version with proofs].

• Tero Laitinen, Tommi Junttila, and Ilkka Niemelä. Classifying and Propagating Parity Constraints. In CP 2012, volume 7514 of Lecture Notes in Computer Science, pages 357-372, Springer, 2012. [bibtex entry].

• Roland Kindermann, Tommi Junttila, and Ilkka Niemelä. SMT-Based Induction Methods for Timed Systems. In FORMATS 2012, volume 7595 of Lecture Notes in Computer Science, pages 171-187, Springer, 2012. [bibtex entry].

• Tero Laitinen, Tommi Junttila, and Ilkka Niemelä. Conflict-Driven XOR-Clause Learning. In SAT 2012, volume 7317 of Lecture Notes in Computer Science, pages 383-396, Springer, 2012. [bibtex entry]. [PDF with proofs]

• Roland Kindermann, Tommi Junttila, and Ilkka Niemelä. Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata. In FMOODS/FORTE 2012, volume 7273 of Lecture Notes in Computer Science, pages 84-100, Springer, 2012. [bibtex entry].

• Tero Laitinen, Tommi Junttila, and Ilkka Niemelä. Equivalence Class Based Parity Reasoning with DPLL(XOR). In ICTAI 2011, pages 649-658, IEEE, 2011. [bibtex entry].

• Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Grid-Based SAT Solving with Iterative Partitioning and Clause Learning. In CP 2011, volume 6876 of Lecture Notes in Computer Science, pages 385-399, Springer, 2011. [bibtex entry].

• Tommi Junttila and Petteri Kaski. Conflict Propagation and Component Recursion for Canonical Labeling. In TAPAS 2011, volume 6595 of Lecture Notes in Computer Science, pages 151-162, Springer, 2011. [bibtex entry].

• Roland Kindermann, Tommi Junttila, and Ilkka Niemelä. Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks. In ACSD 2011, pages 185--194, IEEE, 2011. [bibtex entry].

• Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Partitioning SAT Instances for Distributed Solving. In LPAR-17, volume 6397 of Lecture Notes in Computer Science, pages 372-386, Springer, 2010.

• Tommi Junttila and Petteri Kaski. Exact Cover via Satisfiability: An Empirical Study. In CP 2010, volume 6308 of Lecture Notes in Computer Science, pages 297-304, Springer, 2010.

• Tero Laitinen, Tommi Junttila, and Ilkka Niemelä. Extending Clause Learning DPLL with Parity Reasoning. In ECAI 2010, IOE Press, 2010.

• Tuomas Launiainen, Keijo Heljanko, and Tommi Junttila. Efficient Model Checking of PSL Safety Properties. In ACSD 2010, IEEE, 2010.

• Antti E. J. Hyvärinen, Tommi Junttila, Ilkka Niemelä. Partitioning Search Spaces of a Randomized Search. In AI*IA 2009, volume 5883 of Lecture Notes in Artificial Intelligence, pages 243-252, Springer, 2009. [bibtex entry].

• Alessandro Cimatti, Jori Dubrovin, Tommi Junttila, and Marco Roveri. Structure-Aware Computation of Predicate Abstraction. In FMCAD 2009, pages 9-16, IEEE, 2009. [bibtex entry]

• Tommi Junttila and Jori Dubrovin. Encoding Queues in Satisfiability Modulo Theories based Bounded Model Checking. In LPAR 2008, volume 5330 of Lecture Notes in Computer Science, pages 290-304, Springer, 2008. [bibtex entry]

• Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. Justification-Based Local Search with Adaptive Noise Strategies. In LPAR 2008, volume 5330 of Lecture Notes in Computer Science, pages 31-46, Springer, 2008. [bibtex entry]

• Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Incorporating Learning in Grid-Based Randomized SAT Solving. In: Artificial Intelligence: Methodology, Systems, and Applications (AIMSA 2008), volume 5253 of Lecture Notes in Artificial Intelligence, pages 247-261, Springer, 2008. [bibtex entry]

• Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. Justification-Based Non-Clausal Local Search for SAT. In ECAI 2008, volume 178 of Frontiers in Artificial Intelligence and Applications, pages 353-539, IOS Press, 2008. [bibtex entry]

• Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Strategies for Solving SAT in Grids by Randomized Search. In: AISC/Calculemus/MKM 2008, volume 5144 of Lecture Notes in Computer Science, pages 125-140, Springer, 2008. [bibtex entry]

• Matti Järvisalo and Tommi Junttila. On the Power of Top-Down Branching Heuristics. In Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI-08), AAAI Press, 2008. [ps] [pdf] [bibtex entry]

• Jori Dubrovin and Tommi Junttila. Symbolic Model Checking of Hierarchical UML State Machines. In 8th International Conference on Application of Concurrency to System Design (ACSD 2008), pages 108-117, IEEE Press, 2008. [bibtex entry]

• Jori Dubrovin, Tommi Junttila, and Keijo Heljanko. Symbolic Step Encodings for Object Based Communicating State Machines. In 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, Springer, 2008. [bibtex entry]

• Matti Järvisalo and Tommi Junttila. Limitations of Restricted Branching in Clause Learning. In: CP 2007, volume 4741 of Lecture Notes in Computer Science, pages 348-363, Springer, 2007. [Bibtex Entry]

• Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. A Distribution Method for Solving SAT in Grids. In: SAT 2006, volume 4121 of Lecture Notes in Computer Science, pages 430-435, Springer, 2006. [Bibtex Entry]

• Keijo Heljanko, Tommi Junttila, Misa Keinänen, Martin Lange, and Timo Latvala. Bounded Model Checking for Weak Alternating Büchi Automata. In: CAV 2006, volume 4144 of Lecture Notes in Computer Science, pages 95-108, Springer, 2006. [Bibtex Entry]

• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz, and Roberto Sebastiani. The MathSAT 3 system. In: Automated Deduction - CADE-20, volume 3632 of Lecture Notes in Artificial Intelligence, pages 315-321, Springer, 2005.

• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Silvio Ranise, Peter van Rossum, and Roberto Sebastiani. Efficient Satisfiability Modulo Theories via Delayed Theory Combination. In: CAV 2005, volume 3576 of Lecture Notes in Computer Science, pages 335-349, Springer, 2005.

• Keijo Heljanko, Tommi Junttila, and Timo Latvala. Incremental and Complete Bounded Model Checking for Full PLTL. In: CAV 2005, volume 3576 of Lecture Notes in Computer Science, pages 98-111, Springer, 2005.

• Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz and Roberto Sebastiani. An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. In: Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, volume 3440 of Lecture Notes in Computer Science, pages 317-333, Springer, 2005. [Bibtex Entry]

• Timo Latvala, Armin Biere, Keijo Heljanko and Tommi Junttila. Simple is Better: Efficient Bounded Model Checking for Past LTL. In: R. Cousot (ed.), Verification, Model Checking, and Abstract Interpretation (VMCAI 2005), volume 3385 of Lecture Notes in Computer Science, pages 380-395, Springer, 2005.

• Timo Latvala, Armin Biere, Keijo Heljanko and Tommi Junttila. Simple bounded LTL model checking. In: Alan J. Hu and Andrew K. Martin (eds.), 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, 2004. [Bibtex Entry]

• Tommi A. Junttila. New Canonical Representative Marking Algorithms for Place/Transition-Nets. In J. Cortadella and W. Reisig, editors, Application and Theory of Petri Nets 2004, volume 3099 of Lecture Notes in Computer Science, pages 258-277, Springer, 2004. [Bibtex Entry]

• Tommi A. Junttila. New Orbit Algorithms for Data Symmetries. In Fourth International Conference on Application of Concurrency to System Design (ACSD'04), pages 175-184, IEEE, 2004. [Bibtex Entry]

• Matti Järvisalo, Tommi A. Junttila and Ilkka Niemelä. Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits. In 8th International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida, USA, January 4-6, 2004.

• Tommi A. Junttila and Ilkka Niemelä. Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking. In J. Lloyd et al., editors, Computational Logic - CL 2000; First International Conference, volume 1861 of Lecture Notes in Artificial Intelligence, pages 553-567, London, UK, July 2000. Springer, Berlin. [Gzipped postscript © Springer-Verlag] [PDF © Springer-Verlag] [Bibtex Entry]

Workshop papers

• Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Partitioning SAT Instances for Distributed Solving. In 3rd International Workshop on Logic and Search, 2010.

• Tommi Junttila and Petteri Kaski. Engineering an efficient canonical labeling tool for large and sparse graphs. In: Proceedings of the Ninth Workshop on Algorithm Engineering and Experiments, SIAM, 2007. [Bibtex Entry]

• Toni Jussila, Jori Dubrovin, Tommi Junttila, Timo Latvala, and Ivan Porres. Model Checking Dynamic and Hierarchical UML State Machines. In: 3rd Workshop on Model Development,Validation and Verification (MoDeVa 2006), Genova, Italy, October 2nd, pages 94-110, 2006. [Bibtex Entry]

• Tommi A. Junttila. Towards well-formed algebraic system nets. In H.-D. Burkhard, L. Czaja and P. Starke, editors, Workshop Concurrency, Specification & Programming, number 110 in Informatik-Berichte, pages 116-127. Institut für Informatik, Humboldt-Universität zu Berlin, 1998. [Bibtex Entry] Superseded by the Fundamenta Informaticae paper "Finding symmetries of algebraic system nets".

Unrefereed reports

• Jori Dubrovin and Tommi Junttila. Symbolic Model Checking of Hierarchical UML State Machines. Technical Report HUT-TCS-B23, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, 2007. [ps] [pdf] [bibtex entry]

• Jori Dubrovin, Tommi Junttila, and Keijo Heljanko. Symbolic Step Encodings for Object Based Communicating State Machines. Technical Report HUT-TCS-B24, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, 2007. [ps] [pdf] [bibtex entry]

• 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.

• Tommi Junttila. On the Symmetry Reduction Method for Petri Nets and Similar Formalisms. Research Report A80, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, September 2003. Doctoral dissertation.
  [Gzipped postscript] [PDF] [Bibtex Entry]

• Tommi Junttila. New Canonical Representative Marking Algorithms for Place/Transition-Nets. Research Report A75, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, October 2002. [Gzipped postscript] [PDF] [Bibtex Entry]
  The source code for the extended LoLA analyzer used in obtaining the experimental results in the paper is available here.

• Tommi Junttila. Symmetry Reduction Algorithms for Data Symmetries. Research Report A72, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, May 2002. [Gzipped postscript] [PDF] [Bibtex Entry]

• Tommi Junttila. Computational Complexity of the Place/Transition-Net Symmetry Reduction Method. Research Report A59, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, April 2000. [Gzipped postscript] [PDF] [Bibtex Entry]

• Tommi Junttila. Detecting and Exploiting Data Type Symmetries of Algebraic System Nets during Reachability Analysis. Research Report A57, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 1999. Licentiate's Thesis. [Gzipped postscript] [Bibtex Entry]
  This is an extended version of the Fundamenta Informaticae paper "Finding symmetries of algebraic system nets".

Unpublished draft papers

• Tommi A. Junttila. A note on the computational complexity of a string orbit problem.

  Postscript (289 Kb).