2012 |
|
65 | Roland Kindermann, Tommi Junttila, and Ilkka Niemelä. Beyond lassos: Complete SMT-based bounded model checking for timed automata. In Holger Giese and Grigore Rosu, editors, Formal Techniques for Distributed Systems, volume 7273 of Lecture Notes in Computer Science, pages 84–100. Springer, 2012. |
|
|
64 | Tero Laitinen, Tommi Junttila, and Ilkka Niemelä. Conflict-driven XOR-clause learning. In Alessandro Cimatti and Roberto Sebastiani, editors, Theory and Applications of Satisfiability Testing - SAT 2012, volume 7317 of Lecture Notes in Computer Science, pages 383–396. Springer, 2012. |
|
|
63 | 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. |
|
|
62 | Roland Kindermann, Tommi Junttila, and Ilkka Niemelä. SMT-based induction methods for timed systems. In Marcin Jurdzinski and Dejan Nickovic, editors, Formal Modeling and Analysis of Timed Systems, volume 7595 of Lecture Notes in Computer Science, pages 171–187. Springer, 2012. |
|
|
61 | Tero Laitinen, Tommi Junttila, and Ilkka Niemelä. Classifying and propagating parity constraints. In Michela Milano, editor, Principles and Practice of Constraint Programming - CP 2012, volume 7514 of Lecture Notes in Computer Science, pages 357–372. Springer, 2012. |
|
|
60 | Tero Laitinen, Tommi Junttila, and Ilkka Niemelä. Extending clause learning sat solvers with complete parity reasoning. In ICTAI 2012 - 24th IEEE International Conference on Tools with Artificial Intelligence. IEEE Computer Society Press, 2012. |
|
2011 |
|
59 | Roland Kindermann, Tommi Junttila, and Ilkka Niemelä. Modeling for symbolic analysis of safety instrumented systems with clocks. In 11th International Conference on Application of Concurrency to System Design (ACSD), pages 185–194. IEEE, 2011. |
|
|
58 | Tommi Junttila and Petteri Kaski. Conflict propagation and component recursion for canonical labeling. In A. Marchetti-Spaccamela and M. Segal, editors, Theory and Practice of Algorithms in (Computer) Systems, First International ICST Conference, TAPAS 2011, Rome, Italy, April 18–20, 2011, volume 6595 of Lecture Notes in Computer Science, pages 151–162. Springer, 2011. |
|
|
57 | Antti Eero Johannes Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Grid-based SAT solving with iterative partitioning and clause learning. In Jimmy Ho-Man Lee, editor, Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011. Proceedings, volume 6876 of Lecture Notes in Computer Science, pages 385–399. Springer, 2011. |
|
|
56 | Antti Eero Johannes Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Partitioning search spaces of a randomized search. Fundamenta Informatica, 107(2–3):289–311, 2011. |
|
|
55 | Tero Laitinen, Tommi Junttila, and Ilkka Niemelä. Equivalence class based parity reasoning with dpll(xor). In Taghi M. Khoshgoftaar and Xingquan (Hill) Zhu, editors, ICTAI 2011 - 23rd IEEE International Conference on Tools with Artificial Intelligence, pages 649–658. IEEE Computer Society Press, 2011. |
|
2010 |
|
54 | Tuomas Launiainen, Keijo Heljanko, and Tommi Junttila. Efficient model checking of PSL safety properties. In Tenth International Conference on Application of Concurrency to System Design (ACSD'2010), pages 95–104. IEE Computer Society, 2010. |
|
|
53 | Tommi Junttila and Petteri Kaski. Exact cover via satisfiability: an empirical study. In David Cohen, editor, Proceedings of 16th International Conference on Principles and Practice of Constraint Programming (CP 2010, St. Andrews, Scotland, September 6-10), number 6308 in Lecture Notes in Computer Science, pages 297–304. Springer, 2010. |
|
|
52 | Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Partitioning SAT instances for distributed solving. In Third International Workshop on Logic and Search, pages 1–16, 2010. |
|
|
51 | Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Partitioning SAT instances for distributed solving. In LPAR 2010, volume 6397 of Lecture Notes in Computer Science, pages 372–386. Springer, 2010. |
|
|
50 | Tero Laitinen, Tommi Junttila, and Ilkka Niemelä. Extending clause learning dpll with parity reasoning. In Helder Coelho, Rudi Studer, and Michael Wooldridge, editors, ECAI 2010 - 19th European Conference on Artificial Intelligence, Lisbon, Portugal, August 16-20, 2010, Proceedings, volume 215 of Frontiers in Artificial Intelligence and Applications, pages 21–26. IOS Press, 2010. |
|
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. |
|
