2009 |
|
49 | Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Partitioning search spaces of a randomized search. Technical Report TKK-ICS-R22, Helsinki University of Technology, Department of Information and Computer Science, Espoo, Finland, November 2009. |
|
|
48 | Rolf Drechsler, Tommi Junttila, and Ilkka Niemelä. Non-clausal SAT and ATPG. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, chapter 21, pages 655–693. IOS Press, February 2009. |
|
|
47 | Matti Järvisalo and Tommi Junttila. Limitations of restricted branching in clause learning. Constraints, 14(3):325–356, 2009. |
|
|
46 | Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Incorporating clause learning in grid-based randomized SAT solving. Journal on Satisfiability, Boolean Modeling and Computation, 6:223–244, 2009. |
|
|
45 | Alessandro Cimatti, Jori Dubrovin, Tommi Junttila, and Marco Roveri. Structure-aware computation of predicate abstraction. In FMCAD 2009, pages 9–16. IEEE, 2009. |
|
|
44 | Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Partitioning search spaces of a randomized search. In AI*IA 2009, Lecture Notes in Artificial Intelligence. Springer, 2009. |
|
2008 |
|
43 | Jori Dubrovin and Tommi Junttila. Symbolic model checking of hierarchical UML state machines. In Jonathan Billington, Zhenhua Duan, and Maciej Koutny, editors, Proceedings of the 2008 8th International Conference on Application of Concurrency to System Design, pages 108–117, Xi`an, China, June 23–27 2008. IEEE Press. |
|
|
42 | Jori Dubrovin, Tommi Junttila, and Keijo Heljanko. Symbolic step encodings for object based communicating state machines. In G. Barthe and F. de Boer, editors, FMOODS 2008, volume 5051 of Lecture Notes in Computer Science, pages 96–112. Springer, 2008. |
|
|
41 | Matti Järvisalo and Tommi Junttila. On the power of top-down branching heuristics. In Dieter Fox and Carla P. Gomes, editors, Proceedings of the 23rd AAAI Conference on Artificial Intelligence (AAAI-08), pages 304–309. AAAI Press, 2008. |
|
|
40 | Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Strategies for solving SAT in grids by randomized search. In Serge Autexier, John Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki, and Freek Wiedijk, editors, Intelligent Computer Mathematics (AISC/Calculemus/MKM 2008), volume 5144 of Lecture Notes in Computer Science, pages 125–140. Springer, 2008. |
|
|
39 | Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. Justification-based non-clausal local search for SAT. In Malik Ghallab, Constantine D. Spyropoulos, Nikos Fanotakis, and Nikos Avoukis, editors, Proceedings of the 18th European Conference on Artificial Intelligence (ECAI 2008), volume 178 of Frontiers in Artificial Intelligence and Applications, pages 535–539. IOS Press, 2008. |
|
|
38 | Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Incorporating learning in grid-based randomized SAT solving. In Danail Dochev, Marco Pistore, and Paolo Traverso, editors, Artificial Intelligence: Methodology, Systems, and Applications (AIMSA 2008), volume 5253 of Lecture Notes in Artificial Intelligence, pages 247–261. Springer, 2008. |
|
|
37 | Tommi Junttila and Jori Dubrovin. Encoding queues in satisfiability modulo theories based bounded model checking. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), volume 5330 of Lecture Notes in Artificial Intelligence, pages 290–304. Springer, 2008. |
|
|
36 | Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. Justification-based local search with adaptive noise strategies. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), volume 5330 of Lecture Notes in Artificial Intelligence, pages 31–46. Springer, 2008. |
|
2007 |
|
35 | Jori Dubrovin and Tommi Junttila. Symbolic model checking of hierarchical UML state machines. Technical Report B23, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, December 2007. |
|
|
34 | 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. |
|
|
33 | Tommi Junttila and Petteri Kaski. Engineering an efficient canonical labeling tool for large and sparse graphs. In David Applegate, Gerth Stølting Brodat, Daniel Panario, and Robert Sedgewick, editors, Proceedings of the Ninth Workshop on Algorithm Engineering and Experiments and the Fourth Workshop on Analytic Algorithms and Combinatorics. SIAM, 2007. |
|
|
32 | Matti Järvisalo and Tommi Junttila. Limitations of restricted branching in clause learning. In Christian Bessiere, editor, Principles and Practice of Constraint Programming – CP 2007, volume 4741 of Lecture Notes in Computer Science, pages 348–363. Springer, 2007. |
|
|
31 | Tommi Junttila. SMUML/proco version 2.00 — a translator from UML models to Promela, 2007. Computer program. |
|
|
30 | Tommi Junttila. PySMT version 0.50 — a Python front-end for satisfiability modulo theories solvers, 2007. Computer program. |
|
2006 |
|
29 | 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, October 2006. |
|
|
28 | 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, CAV 2006, volume 4144 of Lecture Notes in Computer Science, pages 95–108. Springer, 2006. |
|
|
27 | Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. A distribution method for solving SAT in grids. In Armin Biere and Carla P. Gomes, editors, SAT 2006, volume 4121 of Lecture Notes in Computer Science, pages 430–435. Springer, 2006. |
|
|
26 | Toni Jussila, Jori Dubrovin, Tommi Junttila, Timo Latvala, and Ivan Porres. Model checking dynamic and hierarchical UML state machines. In MoDeV a: Model Development, Validation and Verification; 3rd International Workshop, Genova, Italy, October 2006, pages 94–110, 2006. |
|
|
25 | 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. |
|
2005 |
|
24 | 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, October 2005. |
|
|
23 | 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. |
|
|
22 | Tommi Junttila. Nusmv-2.2.3-cav2005. Computer program, 2005. |
|
|
21 | Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. Simple is better: Efficient bounded model checking for past LTL. In Radia Cousot, editor, Verification, Model Checking and Abstract Interpretation 2005, 6th International Conference VMCAI'05, Paris, France, volume 3385 of Lecture Notes in Computer Science, pages 380–395. Springer, January 2005. |
|
|
20 | 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 Nicolas Halbwachs and Lenore D. Zuck, editors, 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. |
|
|
19 | Keijo Heljanko, Tommi Junttila, and Timo Latvala. Incremental and complete bounded model checking for full PLTL. In Kousha Etessami and Sriram K. Rajamani, editors, CAV 2005, volume 3576 of Lecture Notes in Computer Science, pages 98–111. Springer, 2005. |
|
|
18 | 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 Kousha Etessami and Sriram K. Rajamani, editors, CAV 2005, volume 3576 of Lecture Notes in Computer Science, pages 335–349. Springer, 2005. |
|
|
17 | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz, and Roberto Sebastiani. The MathSAT 3 system. In Robert Nieuwenhuis, editor, Automated Deduction – CADE-20, volume 3632 of Lecture Notes in Artificial Intelligence, pages 315–321. Springer, 2005. |
|
|
16 | 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 Enrico Giunchiglia and Toby Walsh, editors, SAT 2005; Satisfiability Research in the Year 2005, pages 265–293. Springer, 2005. Reprint of the same article in the number 1-3 of volume 25 of the Journal of Automated Reasoning, 2005. |
|
2004 |
|
15 | Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila. Simple bounded LTL model checking. In Alan Hu and Andy Martin, editors, Formal Methods in Computer-Aided Design 2004, 5th International Conference FMCAD'04, Austin, Texas, USA, volume 3312 of Lecture Notes in Computer Science, pages 186–200. Springer, November 2004. |
|
|
14 | 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. |
|
|
13 | Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä. Unrestricted vs restricted cut in a tableau method for Boolean circuits. AI&M 15–2004, 8th International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida, USA, January 4–6, 2004. Proceedings available at http://rutcor.rutgers.edu/%7Eamai/aimath04/. |
|
|
12 | 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. |
|
|
11 | Tommi A. Junttila. New orbit algorithms for data symmetries. In Application of Concurrency to System Design 2004, pages 175–184. IEEE, 2004. |
|
2003 |
|
10 | 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. |
|
2002 |
|
9 | 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. |
|
|
8 | Tommi Junttila. Symmetry reduction algorithms for data symmetries. Research Report A72, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland, May 2002. |
|
2001 |
|
7 | Tommi A. Junttila. Computational complexity of the Place/Transition-net symmetry reduction method. Journal of Universal Computer Science, 7(4):307–326, 2001. |
|
|
6 | Tommi Junttila. BCSat 0.3 - a satisfiability checker for boolean circuits. Computer program, 2001. |
|
2000 |
|
5 | Tommi A. Junttila and Ilkka Niemelä. Towards an efficient tableau method for Boolean circuit satisfiability checking. In John Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luís Moniz Pereira, Yehoshua Sagiv, and Peter J. Stuckey, 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. |
|
|
4 | 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. |
|
1999 |
|
3 | 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. |
|
|
2 | Tommi A. Junttila. Finding symmetries of algebraic system nets. Fundamenta Informaticae, 37(3):269–289, February 1999. |
|
1998 |
|
1 | 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. |
|
