Tommi A. Junttila

65 papers A* 4A 12B 8Misc 1Journal 21Unranked 16

Year	Rank	Type	Title / Venue / Authors
2022	—	`conf`	Formal Analysis of Lending Pools in Decentralized Finance. ISoLA (3) Massimo Bartoletti, James Hsin-yu Chiang, Tommi A. Junttila, Alberto Lluch-Lafuente, Massimiliano Mirelli, Andrea Vandin
2022	J	`jnl`	Formal Analysis of Lending Pools in Decentralized Finance. CoRR Massimo Bartoletti, James Hsin-yu Chiang, Tommi A. Junttila, Alberto Lluch-Lafuente, Massimiliano Mirelli, Andrea Vandin
2021	—	`ch.`	Non-Clausal SAT and ATPG. Handbook of Satisfiability Rolf Drechsler, Tommi A. Junttila, Ilkka Niemelä
2020	J	`jnl`	An adaptive prefix-assignment technique for symmetry reduction. J. Symb. Comput. Tommi A. Junttila, Matti Karppa, Petteri Kaski, Jukka Kohonen
2017	A	`conf`	An Adaptive Prefix-Assignment Technique for Symmetry Reduction. SAT Tommi A. Junttila, Matti Karppa, Petteri Kaski, Jukka Kohonen
2017	J	`jnl`	An adaptive prefix-assignment technique for symmetry reduction. CoRR Tommi A. Junttila, Matti Karppa, Petteri Kaski, Jukka Kohonen
2014	J	`jnl`	Classifying and Propagating Parity Constraints (extended version). CoRR Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä
2014	J	`jnl`	Conflict-Driven XOR-Clause Learning (extended version). CoRR Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä
2013	J	`jnl`	Bounded Model Checking of an MITL Fragment for Timed Automata CoRR Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä
2013	—	`conf`	Bounded Model Checking of an MITL Fragment for Timed Automata. ACSD Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä
2013	J	`jnl`	Simulating Parity Reasoning (extended version). CoRR Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä
2013	B	`conf`	Simulating Parity Reasoning. LPAR Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä
2012	—	`conf`	Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata. FMOODS/FORTE Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä
2012	A	`conf`	Classifying and Propagating Parity Constraints. CP Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä
2012	A	`conf`	Conflict-Driven XOR-Clause Learning. SAT Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä
2012	J	`jnl`	Exploiting step semantics for efficient bounded model checking of asynchronous systems. Sci. Comput. Program. Jori Dubrovin, Tommi A. Junttila, Keijo Heljanko
2012	J	`jnl`	Extending Clause Learning SAT Solvers with Complete Parity Reasoning (extended version) CoRR Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä
2012	B	`conf`	Extending Clause Learning SAT Solvers with Complete Parity Reasoning. ICTAI Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä
2012	—	`conf`	SMT-Based Induction Methods for Timed Systems. FORMATS Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä
2012	J	`jnl`	SMT-based Induction Methods for Timed Systems CoRR Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä
2011	—	`conf`	Conflict Propagation and Component Recursion for Canonical Labeling. TAPAS Tommi A. Junttila, Petteri Kaski
2011	J	`jnl`	Efficient model checking of PSL safety properties. IET Comput. Digit. Tech. Tuomas Launiainen, Keijo Heljanko, Tommi A. Junttila
2011	B	`conf`	Equivalence Class Based Parity Reasoning with DPLL(XOR). ICTAI Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä
2011	A	`conf`	Grid-Based SAT Solving with Iterative Partitioning and Clause Learning. CP Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä
2011	—	`conf`	Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks. ACSD Roland Kindermann, Tommi A. Junttila, Ilkka Niemelä
2011	J	`jnl`	Partitioning Search Spaces of a Randomized Search. Fundam. Informaticae Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä
2010	—	`conf`	Efficient Model Checking of PSL Safety Properties. ACSD Tuomas Launiainen, Keijo Heljanko, Tommi A. Junttila
2010	A	`conf`	Exact Cover via Satisfiability: An Empirical Study. CP Tommi A. Junttila, Petteri Kaski
2010	A	`conf`	Extending Clause Learning DPLL with Parity Reasoning. ECAI Tero Laitinen, Tommi A. Junttila, Ilkka Niemelä
2010	—	`conf`	Partitioning SAT Instances for Distributed Solving. LPAR (Yogyakarta) Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä
2009	J	`jnl`	Incorporating Clause Learning in Grid-Based Randomized SAT Solving. J. Satisf. Boolean Model. Comput. Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä
2009	J	`jnl`	Limitations of restricted branching in clause learning. Constraints An Int. J. Matti Järvisalo, Tommi A. Junttila
2009	—	`ch.`	Non-Clausal SAT and ATPG. Handbook of Satisfiability Rolf Drechsler, Tommi A. Junttila, Ilkka Niemelä
2009	—	`conf`	Partitioning Search Spaces of a Randomized Search. AI*IA Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä
2009	B	`conf`	Structure-aware computation of predicate abstraction. FMCAD Alessandro Cimatti, Jori Dubrovin, Tommi A. Junttila, Marco Roveri
2008	B	`conf`	Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking. LPAR Tommi A. Junttila, Jori Dubrovin
2008	Misc	`conf`	Incorporating Learning in Grid-Based Randomized SAT Solving. AIMSA Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä
2008	B	`conf`	Justification-Based Local Search with Adaptive Noise Strategies. LPAR Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä
2008	A	`conf`	Justification-Based Non-Clausal Local Search for SAT. ECAI Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä
2008	A*	`conf`	On the Power of Top-Down Branching Heuristics. AAAI Matti Järvisalo, Tommi A. Junttila
2008	—	`conf`	Strategies for Solving SAT in Grids by Randomized Search. AISC/MKM/Calculemus Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä
2008	—	`conf`	Symbolic Step Encodings for Object Based Communicating State Machines. FMOODS Jori Dubrovin, Tommi A. Junttila, Keijo Heljanko
2008	—	`conf`	Symbolic model checking of hierarchical UML state machines. ACSD Jori Dubrovin, Tommi A. Junttila
2007	A	`conf`	Engineering an Efficient Canonical Labeling Tool for Large and Sparse Graphs. ALENEX Tommi A. Junttila, Petteri Kaski
2007	A	`conf`	Limitations of Restricted Branching in Clause Learning. CP Matti Järvisalo, Tommi A. Junttila
2006	A	`conf`	A Distribution Method for Solving SAT in Grids. SAT Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä
2006	A*	`conf`	Bounded Model Checking for Weak Alternating Büchi Automata. CAV Keijo Heljanko, Tommi A. Junttila, Misa Keinänen, Martin Lange, Timo Latvala
2006	J	`jnl`	Efficient theory combination via boolean search. Inf. Comput. Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani
2006	J	`jnl`	Linear Encodings of Bounded LTL Model Checking CoRR Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan
2006	J	`jnl`	Linear Encodings of Bounded LTL Model Checking. Log. Methods Comput. Sci. Armin Biere, Keijo Heljanko, Tommi A. Junttila, Timo Latvala, Viktor Schuppan
2005	A	`conf`	An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. TACAS Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
2005	A*	`conf`	Efficient Satisfiability Modulo Theories via Delayed Theory Combination. CAV Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Silvio Ranise, Peter van Rossum, Roberto Sebastiani
2005	A*	`conf`	Incremental and Complete Bounded Model Checking for Full PLTL. CAV Keijo Heljanko, Tommi A. Junttila, Timo Latvala
2005	J	`jnl`	MathSAT: Tight Integration of SAT and Mathematical Decision Procedures. J. Autom. Reason. Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
2005	B	`conf`	Simple Is Better: Efficient Bounded Model Checking for Past LTL. VMCAI Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila
2005	A	`conf`	The MathSAT 3 System. CADE Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani
2005	J	`jnl`	Unrestricted vs restricted cut in a tableau method for Boolean circuits. Ann. Math. Artif. Intell. Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä
2004	—	`conf`	New Canonical Representative Marking Algorithms for Place/Transition-Nets. ICATPN Tommi A. Junttila
2004	—	`conf`	New Orbit Algorithms for Data Symmetries. ACSD Tommi A. Junttila
2004	B	`conf`	Simple Bounded LTL Model Checking. FMCAD Timo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila
2004	—	`conf`	Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits. AI&M Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä
2003	—	`—`	On the symmetry reduction method for Petri nets and similar formalisms. Tommi A. Junttila
2001	J	`jnl`	Computational Complexity of the Place/Transition-Net Symmetry Reduction Method. J. Univers. Comput. Sci. Tommi A. Junttila
2000	—	`conf`	Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking. Computational Logic Tommi A. Junttila, Ilkka Niemelä
1999	J	`jnl`	Finding Symmetries of Algebraic System Nets. Fundam. Informaticae Tommi A. Junttila