Tommi A. Junttila

Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä: Bounded Model Checking of an MITL Fragment for Timed Automata. CoRR abs/1304.7209 (2013)

Jori Dubrovin, Tommi A. Junttila, Keijo Heljanko: Exploiting step semantics for efficient bounded model checking of asynchronous systems. Sci. Comput. Program. 77(10-11): 1095-1121 (2012)

Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä: Classifying and Propagating Parity Constraints. CP 2012: 357-372

Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä: SMT-Based Induction Methods for Timed Systems. FORMATS 2012: 171-187

Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä: Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata. FMOODS/FORTE 2012: 84-100

Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä: Extending Clause Learning SAT Solvers with Complete Parity Reasoning. ICTAI 2012: 65-72

Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä: Conflict-Driven XOR-Clause Learning. SAT 2012: 383-396

Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä: SMT-based Induction Methods for Timed Systems. CoRR abs/1204.5639 (2012)

Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä: Extending Clause Learning SAT Solvers with Complete Parity Reasoning (extended version). CoRR abs/1207.0988 (2012)

Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä: Partitioning Search Spaces of a Randomized Search. Fundam. Inform. 107(2-3): 289-311 (2011)

Tuomas Launiainen, Keijo Heljanko, Tommi A. Junttila: Efficient model checking of PSL safety properties. IET Computers & Digital Techniques 5(6): 479-492 (2011)

Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä: Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks. ACSD 2011: 185-194

Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä: Grid-Based SAT Solving with Iterative Partitioning and Clause Learning. CP 2011: 385-399

Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä: Equivalence Class Based Parity Reasoning with DPLL(XOR). ICTAI 2011: 649-658

Tommi A. Junttila, Petteri Kaski: Conflict Propagation and Component Recursion for Canonical Labeling. TAPAS 2011: 151-162

Tuomas Launiainen, Keijo Heljanko, Tommi A. Junttila: Efficient Model Checking of PSL Safety Properties. ACSD 2010: 95-104

Tommi A. Junttila, Petteri Kaski: Exact Cover via Satisfiability: An Empirical Study. CP 2010: 297-304

Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä: Extending Clause Learning DPLL with Parity Reasoning. ECAI 2010: 21-26

Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä: Partitioning SAT Instances for Distributed Solving. LPAR (Yogyakarta) 2010: 372-386

Matti Järvisalo, Tommi A. Junttila: Limitations of restricted branching in clause learning. Constraints 14(3): 325-356 (2009)

Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä: Incorporating Clause Learning in Grid-Based Randomized SAT Solving. JSAT 6(4): 223-244 (2009)

Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä: Partitioning Search Spaces of a Randomized Search. AI*IA 2009: 243-252

Alessandro Cimatti, Jori Dubrovin, Tommi A. Junttila, Marco Roveri: Structure-aware computation of predicate abstraction. FMCAD 2009: 9-16

Rolf Drechsler, Tommi A. Junttila, Ilkka Niemelä: Non-Clausal SAT and ATPG. Handbook of Satisfiability 2009: 655-693

Matti Järvisalo, Tommi A. Junttila: On the Power of Top-Down Branching Heuristics. AAAI 2008: 304-309

Jori Dubrovin, Tommi A. Junttila: Symbolic model checking of hierarchical UML state machines. ACSD 2008: 108-117

Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä: Incorporating Learning in Grid-Based Randomized SAT Solving. AIMSA 2008: 247-261

Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä: Strategies for Solving SAT in Grids by Randomized Search. AISC/MKM/Calculemus 2008: 125-140

Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä: Justification-Based Non-Clausal Local Search for SAT. ECAI 2008: 535-539

Jori Dubrovin, Tommi A. Junttila, Keijo Heljanko: Symbolic Step Encodings for Object Based Communicating State Machines. FMOODS 2008: 96-112

Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä: Justification-Based Local Search with Adaptive Noise Strategies. LPAR 2008: 31-46

Tommi A. Junttila, Jori Dubrovin: Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking. LPAR 2008: 290-304

Tommi A. Junttila, Petteri Kaski: Engineering an Efficient Canonical Labeling Tool for Large and Sparse Graphs. ALENEX 2007

Matti Järvisalo, Tommi A. Junttila: Limitations of Restricted Branching in Clause Learning. CP 2007: 348-363

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani: Efficient theory combination via boolean search. Inf. Comput. 204(10): 1493-1525 (2006)

Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan: Linear Encodings of Bounded LTL Model Checking. Logical Methods in Computer Science 2(5) (2006)

Keijo Heljanko, Tommi A. Junttila, Misa Keinänen, Martin Lange, Timo Latvala: Bounded Model Checking for Weak Alternating Büchi Automata. CAV 2006: 95-108

Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä: A Distribution Method for Solving SAT in Grids. SAT 2006: 430-435

Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan: Linear Encodings of Bounded LTL Model Checking. CoRR abs/cs/0611029 (2006)

Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä: Unrestricted vs restricted cut in a tableau method for Boolean circuits. Ann. Math. Artif. Intell. 44(4): 373-399 (2005)

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. J. Autom. Reasoning 35(1-3): 265-293 (2005)

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: The MathSAT 3 System. CADE 2005: 315-321

Keijo Heljanko, Tommi A. Junttila, Timo Latvala: Incremental and Complete Bounded Model Checking for Full PLTL. CAV 2005: 98-111

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani: Efficient Satisfiability Modulo Theories via Delayed Theory Combination. CAV 2005: 335-349

Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani: An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. TACAS 2005: 317-333

Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila: Simple Is Better: Efficient Bounded Model Checking for Past LTL. VMCAI 2005: 380-395

Tommi A. Junttila: New Orbit Algorithms for Data Symmetries. ACSD 2004: 175-184

Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä: Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits. AMAI 2004

Tommi A. Junttila: New Canonical Representative Marking Algorithms for Place/Transition-Nets. ICATPN 2004: 258-277

Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila: Simple Bounded LTL Model Checking. FMCAD 2004: 186-200

Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä: Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits. ISAIM 2004

Tommi A. Junttila: Computational Complexity of the Place/Transition-Net Symmetry Reduction Method. J. UCS 7(4): 307-326 (2001)

Tommi A. Junttila, Ilkka Niemelä: Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking. Computational Logic 2000: 553-567

Tommi A. Junttila: Finding Symmetries of Algebraic System Nets. Fundam. Inform. 37(3): 269-289 (1999)