Tommi Junttila

  • Aalto SCI Computer Science Konemiehentie 2

19982019

Research output per year

If you made any changes in Pure these will be visible here soon.

Research Output

2019

An adaptive prefix-assignment technique for symmetry reduction

Junttila, T., Karppa, M., Kaski, P. & Kohonen, J., Jul 2019, In : JOURNAL OF SYMBOLIC COMPUTATION. 99, p. 21-49

Research output: Contribution to journalArticleScientificpeer-review

Open Access
File
20 Downloads (Pure)
2017

An adaptive prefix-assignment technique for symmetry reduction

Junttila, T., Karppa, M., Kaski, P. & Kohonen, J., 2017, Theory and Applications of Satisfiability Testing – SAT 2017 - 20th International Conference, Proceedings. p. 101-118 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10491 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

1 Citation (Scopus)
2013

Bounded Model Checking of an MITL Fragment for Timed Automata

Kindermann, R., Junttila, T. & Niemelä, I., 2013, 13th International Conference on Application of Concurrency to System Design (ACSD), July 8-10, Barcelona, Spain. IEEE, p. 216-225

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

7 Citations (Scopus)

Simulating Parity Reasoning

Laitinen, T., Junttila, T. & Niemelä, I., 2013, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-19, Stellenbosch, South Africa, 15-19th December 2013. p. 568-583 (Lecture Notes in Computer Science; vol. 8312).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

1 Citation (Scopus)
2012

Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata

Kindermann, R., Junttila, T. & Niemelä, I., 2012, FMOODS FORTE IFIP International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE 2012) FMOODS FORTE, Stockholm, Sweden, June 13-16, 2012. Giese, H. & Rosu, G. (eds.). p. 84-100 (Lecture Notes in Computer Science; vol. 7273).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

11 Citations (Scopus)

Classifying and Propagating Parity Constraints

Laitinen, T., Junttila, T. & Niemelä, I., 2012, 18th International Conference on Principles and Practice of Constraint Programming (CP 2012), Quebec City, Canada, October 8-12, 2012. Milano, M. (ed.). p. 357-372 (Lecture Notes in Computer Science; vol. 7514).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

4 Citations (Scopus)

Conflict-Driven XOR-Clause Learning

Laitinen, T., Junttila, T. & Niemelä, I., 2012, Fifteenth International Conference on Theory and Applications of Satisfiability Testing (SAT 2012), Trento, Italy, June 17-20, 2012. Cimatti, A. & Sebastiani, R. (eds.). p. 383-396 ( Lecture Notes in Computer Science; vol. 7317).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

6 Citations (Scopus)

Exploiting step semantics for efficient bounded model checking of asynchronous systems

Dubrovin, J., Junttila, T. & Heljanko, K., 2012, In : Science of Computer Programming. 77, 10-11, p. 1095-1121

Research output: Contribution to journalArticleScientificpeer-review

6 Citations (Scopus)

Extending Clause Learning SAT Solvers with Complete Parity Reasoning

Laitinen, T., Junttila, T. & Niemelä, I., 2012, 2012 IEEE 24th International Conference on Tools with Artificial Intelligence, ICTAI 2012. IEEE, Vol. 1. p. 65-72 8 p. 6495030. (Proceedings-International Conference on Tools With Artificial Intelligence).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

4 Citations (Scopus)

SMT-Based Induction Methods for Timed Systems

Kindermann, R., Junttila, T. & Niemelä, I., 2012, 10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2012), London, UK, September 18-20, 2012. Jurdzinski, M. & Nickovic, D. (eds.). p. 171-187 (Lecture Notes in Computer Science; vol. 7595).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

19 Citations (Scopus)
2011

Conflict Propagation and Component Recursion for Canonical Labeling

Junttila, T. & Kaski, P., 2011, TAPAS Theory and Practice of Algorithms in (Computer) Systems, First International ICST Conference, TAPAS 2011, Rome, Italy, April 18-20, 2011. Marchetti-Spaccamela, A. & Segal, M. (eds.). p. 151-162

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

19 Citations (Scopus)

Efficient Model Checking of PSL Safety Properties

Launiainen, T., Heljanko, K. & Junttila, T., 2011, In : IET COMPUTERS AND DIGITAL TECHNIQUES. 5, 6, p. 479-492

Research output: Contribution to journalArticleScientificpeer-review

Equivalence Class Based Parity Reasoning with DPLL(XOR)

Laitinen, T., Junttila, T. & Niemelä, I., 2011, 23rd IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2011). Khoshgoftaar, T. M. & Zhu, X. (eds.). IEEE, p. 649-658 (International Conference on Tools with Artificial Intelligence. Proceedings).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

7 Citations (Scopus)

Grid-Based SAT Solving with Iterative Partitioning and Clause Learning

Hyvärinen, A. E. J., Junttila, T. & Niemelä, I., 2011, 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011. p. 385-399 (Lecture Notes in Computer Science; vol. 6876).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

21 Citations (Scopus)

Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks

Kindermann, R., Junttila, T. & Niemelä, I., 2011, 11th International Conference on Application of Concurrency to System Designg, (ACSD 2011). IEEE, p. 185-194 (International Conference on Application of Concurrency to System Design. Proceedings ).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

4 Citations (Scopus)

Partitioning Search Spaces of a Randomized Search

Hyvärinen, A. E. J., Junttila, T. & Niemelä, I., 2011, In : Fundamenta Informaticae. 107, 2-3, p. 289-311

Research output: Contribution to journalArticleScientificpeer-review

11 Citations (Scopus)
2010

Efficient Model Checking of PSL Safety Properties

Launiainen, T., Heljanko, K. & Junttila, T., 2010, The 10th International Conference on Application of Concurrency to System Design (ACSD'2010). Braga, p. 95-104

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

9 Citations (Scopus)

Exact cover via satisfiability: an empirical study

Junttila, T. & Kaski, P., 2010, 16th International Conference on Principles and Practice of Constraint Programming (CP 2010, St. Andrews, Scotland, September6-10). Cohen, D. (ed.). p. 297-304

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

3 Citations (Scopus)

Extending Clause Learning DPLL with Parity Reasoning

Laitinen, T., Junttila, T. A. & Niemelä, I., 2010, 19th European Conference on Artificial Intelligence (ECAI 2010), Lisbon, Portugal, August 16-20, 2010. Coelho, H., Studer, R. & Wooldridge, M. (eds.). IOS PRESS, p. 21-26 (Frontiers in Artificial Intelligence and Applications; vol. 215).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

11 Citations (Scopus)

Partitioning SAT Instances for Distributed Solving

Hyvärinen, A. E. J., Junttila, T. & Niemelä, I., 2010, Logic for Programming, Artificial Intelligence, and Reasoning: 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Fermüller, C. G. & Voronkov, A. (eds.). p. 372-386 15 p. (Lecture Notes in Computer Science; vol. 6397 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

25 Citations (Scopus)
2009

Incorporating Clause Learning in Grid-Based Randomized SAT Solving

Hyvärinen, A. E. J., Junttila, T. & Niemelä, I., 2009, In : Journal of Satisfiability, Boolean Modeling and Computation. 6, p. 223-244

Research output: Contribution to journalArticleScientificpeer-review

Limitations of Restricted Branching in Clause Learning

Järvisalo, M. & Junttila, T., 2009, In : Constraints. 14, 3, p. 325-356

Research output: Contribution to journalArticleScientificpeer-review

17 Citations (Scopus)

Non-Clausal SAT and ATPG

Drechsler, R., Junttila, T. & Niemelä, I., 2009, Handbook of Satisfiability. Biere, A., Heule, M. J. H., van Maaren, H. & Walsh, T. (eds.). IOS PRESS, p. 655-693 39 p. (Frontiers in Artificial Intelligence and Applications; vol. 185, no. 1).

Research output: Chapter in Book/Report/Conference proceedingChapterScientificpeer-review

6 Citations (Scopus)

Partitioning Search Spaces of a Randomized Search

Hyvärinen, A. E. J., Junttila, T. & Niemelä, I., 2009, AI*IA 2009: Emergent Perspectives in Artificial Intelligence : XIth International Conference of the Italian Association for Artificial Intelligence Reggio Emilia, Italy, December 9-12, 2009 Proceedings. Serra, R. & Cucchiara, R. (eds.). p. 243-252 (Lecture Notes in Computer Science ; vol. 5883).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

8 Citations (Scopus)

Partitioning Search Spaces of a Randomized Search

Hyvärinen, A. E. J., Junttila, T. & Niemelä, I., 2009, Espoo. 22 p. (TKK reports in information and computer science; no. TKK-ICS-R22)

Research output: Book/ReportCommissioned reportProfessional

Structure-Aware Computation of Predicate Abstraction

Cimatti, A., Dubrovin, J., Junttila, T. & Roveri, M., 2009, The 9th International Conference on Formal Methods in Computer Aided Design (FMCAD'09). Biere, A. & Pixley, C. (eds.). IEEE, p. 9-16

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

9 Citations (Scopus)
2008

Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking

Junttila, T. & Dubrovin, J., 2008, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08). Cervesato, I., Veith, H. & Voronkov, A. (eds.). p. 290-304

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

3 Citations (Scopus)

Incorporating Learning in Grid-Based Randomized SAT Solving

Hyvärinen, A. E. J., Junttila, T. & Niemelä, I., 2008, Artificial Intelligence: Methodology, Systems, and Applications : 13th International Conference, AIMSA 2008, Varna, Bulgaria, September 4-6, 2008. Proceedings. Dochev, D., Pistore, M. & Traverso, P. (eds.). p. 247-261 (Lecture Notes in Computer Science ; vol. 5253).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

6 Citations (Scopus)

Justification-Based Local Search with Adaptive Noise Strategies

Järvisalo, M., Junttila, T. & Niemelä, I., 2008, Logic for Programming, Artificial Intelligence, and Reasoning : 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings. Cervesato, I., Veith, H. & Voronkov, A. (eds.). p. 31-46 (Lecture Notes in Computer Science ; vol. 5330).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

3 Citations (Scopus)

Justification-Based Non-Clausal Local Search for SAT

Järvisalo, M., Junttila, T. & Niemelä, I., 2008, ECAI 2008: 18th European Conference on Artificial Intelligence (ECAI 2008), Patras, Greece, 21.-25.7.2008. Ghallab, M., Spyropoulos, C. D., Fanotakis, N. & Avoukis, N. (eds.). IOS PRESS, p. 535-539 (Frontiers in Artificial Intelligence and Applications; vol. 178).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

On the power of top-down branching heuristics

Järvisalo, M. & Junttila, T., 2008, 23rd AAAI Conference on Artificial Intelligence, Chicago, Illinois, USA, July 13-17, 2008. AAAI PRESS, p. 304-309

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

3 Citations (Scopus)

Strategies for Solving SAT in Grids by randomized search

Hyvärinen, A. E. J., Junttila, T. & Niemelä, I., 2008, Intelligent Computer Mathematics : 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings. Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M. & Wiedijk, F. (eds.). p. 125-140 (Lecture Notes in Computer Science; vol. 5144).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

8 Citations (Scopus)

Symbolic Model Checking of Hierarchical UML State Machines

Dubrovin, J. & Junttila, T., 2008, The 8th International Conference on Application of Concurrency to System Design (ACSD'08). Billington, J., Duan, Z. & Koutny, M. (eds.). IEEE Press, p. 108-117

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

21 Citations (Scopus)

Symbolic Step Encodings for Object Based Communicating State Machines

Dubrovin, J., Junttila, T. & Heljanko, K., 2008, Formal Methods for Open Object-based Distributed Systems (FMOODS'08). Barthe, G. & de Boer, F. S. (eds.). Oslo, Norway, p. 96-112

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

9 Citations (Scopus)
2007

Engineering an efficient canonical labeling tool for large and sparse graphs

Junttila, T. & Kaski, P., 2007, The Ninth Workshop on Algorithm Engineering and Experiments and the Fourth Workshop on Analytic Algorithms and Combinatorics. Applegate, D., Brodat, G. S., Panario, D. & Sedgewick, R. (eds.).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

118 Citations (Scopus)

Limitations of Restricted Branching in Clause Learning

Järvisalo, M. & Junttila, T., 2007, 13th International Conference on Principles and Practice of Constraint Programming (CP'07), Providence, Rhode Island, USA, 23-27.9.2007. Bessiere, C. (ed.). p. 348-363

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

5 Citations (Scopus)

PySMT version 0.50 - a Python front-end for satisfiability modulo theories solvers

Junttila, T., 2007

Research output: Artistic and non-textual formSoftwareScientific

SMUML/proco version 2.00 - a translator from UML models to Promela

Junttila, T., 2007

Research output: Artistic and non-textual formSoftwareScientific

Symbolic Model Checking of Hierarchical UML State Machines

Dubrovin, J. & Junttila, T., 2007, Espoo, (Helsinki University of Technology Laboratory for Theoretical Computer Science Technical Reports; no. B23).

Research output: Working paperProfessional

21 Citations (Scopus)

Symbolic Step Encodings for Object Based Communicating State Machines

Dubrovin, J., Junttila, T. & Heljanko, K., 2007, Espoo, (Helsinki University of Technology Laboratory for Theoretical Computer Science Technical Reports; no. B24).

Research output: Working paperProfessional

9 Citations (Scopus)
2006

A Distribution Method for Solving SAT in Grids

Hyvärinen, A. E. J., Junttila, T. & Niemelä, I., 2006, Theory and Applications of Satisfiability Testing - SAT 2006 : 9th International Conference, Seattle, WA, USA, August 12-15, 2006. Proceedings. Biere, A. & P. Gomes, C. (eds.). p. 430-435 (Lecture Notes in Computer Science ; vol. 4121).

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

21 Citations (Scopus)

BC package - tools for constrained Boolean circuits

Junttila, T., 2006

Research output: Artistic and non-textual formSoftwareScientific

bliss- a canonical labeling tool for graphs

Junttila, T., 2006

Research output: Artistic and non-textual formSoftwareScientific

Bounded Model Checking for Weak Alternating Buchi Automata

Heljanko, K., Junttila, T., Keinänen, M., Lange, M. & Latvala, T., 2006, Computer Aided Verification 2006, Seattle, WA, USA, 17.-20.8.2006. Ball, T. & Jones, R. B. (eds.). p. 95-108

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

15 Citations (Scopus)

Efficient theory combination via boolean search

Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Ranise, S., van Rossum, P. & Sebastiani, R., 2006, In : Information and Computation. 204, 10, p. 1493-1525

Research output: Contribution to journalArticleScientificpeer-review

41 Citations (Scopus)

Linear Encodings of Bounded LTL Model Checking

Biere, A., Heljanko, K., Junttila, T., Latvala, T. & Schuppan, V., 2006, In : LOGICAL METHODS IN COMPUTER SCIENCE. 2, 5:5, p. 1-64

Research output: Contribution to journalArticleScientificpeer-review

MathSAT: Tight Integration of SAT and mathematical decision procedures

Junttila, T., Bozzano, M., Bruttomesso, R., Cimatti, A., van Rossum, P., Schulz, S. & Sebastiani, R., 2006, SAT 2005; Satisfiability Research in the Year 2005. Giunchiglia, E. & Walsh, T. (eds.). Berlin, p. 265-293

Research output: Chapter in Book/Report/Conference proceedingChapterScientificpeer-review

40 Citations (Scopus)

Model Checking Dynamic and Hierarchical UML State Machines

Jussila, T., Dubrovin, J., Junttila, T., Latvala, T. & Porres, I., 2006, 3rd Workshop on Model Design and Validation (MoDeVa 2006), Genova, Italy, October 2nd 2006. p. 94-110

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

NuSMV-2.3.99-CAV2006

Latvala, T. & Junttila, T., 2006

Research output: Artistic and non-textual formSoftwareScientific

2005

An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic

Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S. & Sebastiani, R., 2005, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), April 4-8, 2005, Edinburgh, U.K.. Halbwachs, N. & Zuck, L. (eds.). p. 317-333

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

44 Citations (Scopus)