Tommi Junttila (Senior University Lecturer, Doctor of Science, Docent)
Contact information:
Postal address:
Office:
room C312,
Computer Science Building,
Konemiehentie 2,
Espoo
E-mail: firstname.lastname@aalto.fiOffice hours: by appointment
Theses supervised and instructed ▼
Supervised:
Instructed:
Sokoban-pulmien ratkaiseminen
Integrating Stratum and A+ Functionalities in Moodle: Architecture and Evaluation
Extending SAT Solver with Parity Reasoning
SMT-based Verification of Timed Systems and Software .
Doctoral dissertation of Roland Kindermann.
Aalto University, 2014.
Grid Based Propositional Satisfiability Solving
Efficient Symbolic Model Checking of Concurrent Systems
Extending SAT Solver with Parity Constraints .
Master's thesis of Tero Laitinen.
Aalto University, 2010.
Approaches to Grid-Based SAT Solving .
Licentiate's thesis of Antti Hyvärinen.
Helsinki University of Technology, 2009.
Structure-Based Satisfiability Checking: Analyzing and Harnessing the Potential
Impact of Restricted Branching on Clause Learning SAT Solving .
Licentiate's thesis of Matti Järvisalo.
Helsinki University of Technology, 2007.
SATU: A system for distributed propositional satisfiability checking in computational grids .
Master's thesis of Antti Hyvärinen.
Helsinki University of Technology, 2005.
Proof Complexity of Cut-Based Tableaux for Boolean Circuit Satisfiability Checking .
Master's thesis of Matti Järvisalo.
Helsinki University of Technology, 2004.
Some software ▼
bliss —
An open source tool for computing automorphism groups and canonical forms of graphs.
Constrained Boolean circuits —
A file format and some tools for solving constrained Boolean circuit satisfiability.
pdf2video —
A tool for making Amazon Polly narrated video presentations from PDF files.
SMurphi —
An extended version of the Murphi verifier including three new symmetry reduction algorithms.
TJLoLA —
An extended version of the LoLA analyzer including three new symmetry reduction algorithms.
Publications ▼
Massimo Bartoletti, James Chiang, Tommi Junttila, Alberto Lluch Lafuente, Massimiliano Mirelli, and Andrea Vandin: Formal Analysis of Lending Pools in Decentralized Finance
Tommi Junttila, Matti Karppa, Petteri Kaski, and Jukka Kohonen: An adaptive prefix-assignment technique for symmetry reduction
Tommi Junttila, Matti Karppa, Petteri Kaski, and Jukka Kohonen: An Adaptive Prefix-Assignment Technique for Symmetry Reduction
Tommi Junttila, Matti Karppa, Petteri Kaski, and Jukka Kohonen: An adaptive prefix-assignment technique for symmetry reduction
Tero Laitinen, Tommi Junttila, and Ilkka Niemelä: Classifying and Propagating Parity Constraints (extended version)
Tero Laitinen, Tommi Junttila, and Ilkka Niemelä: Conflict-Driven XOR-Clause Learning (extended version)
Roland Kindermann, Tommi Junttila, and Ilkka Niemelä: Bounded Model Checking of an MITL Fragment for Timed Automata
Tero Laitinen, Tommi Junttila, and Ilkka Niemelä: Simulating Parity Reasoning
Roland Kindermann, Tommi Junttila, and Ilkka Niemelä: Bounded Model Checking of an MITL Fragment for Timed Automata
Tero Laitinen, Tommi Junttila, and Ilkka Niemelä: Simulating Parity Reasoning (extended version)
Jori Dubrovin, Tommi Junttila, and Keijo Heljanko: Exploiting step semantics for efficient bounded model checking of asynchronous systems
Tero Laitinen, Tommi Junttila, and Ilkka Niemelä: Classifying and Propagating Parity Constraints
Roland Kindermann, Tommi Junttila, and Ilkka Niemelä: SMT-Based Induction Methods for Timed Systems
Roland Kindermann, Tommi Junttila, and Ilkka Niemelä: Beyond Lassos: Complete SMT-Based Bounded Model Checking for Timed Automata
Tero Laitinen, Tommi Junttila, and Ilkka Niemelä: Extending Clause Learning SAT Solvers with Complete Parity Reasoning
Tero Laitinen, Tommi Junttila, and Ilkka Niemelä: Conflict-Driven XOR-Clause Learning
Roland Kindermann, Tommi Junttila, and Ilkka Niemelä: SMT-based Induction Methods for Timed Systems
Tero Laitinen, Tommi Junttila, and Ilkka Niemelä: Extending Clause Learning SAT Solvers with Complete Parity Reasoning (extended version)
Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä: Partitioning Search Spaces of a Randomized Search
Tuomas Launiainen, Keijo Heljanko, and Tommi Junttila: Efficient model checking of PSL safety properties
Roland Kindermann, Tommi Junttila, and Ilkka Niemelä: Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks
Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä: Grid-Based SAT Solving with Iterative Partitioning and Clause Learning
Tero Laitinen, Tommi Junttila, and Ilkka Niemelä: Equivalence Class Based Parity Reasoning with DPLL(XOR)
Tommi Junttila, and Petteri Kaski: Conflict Propagation and Component Recursion for Canonical Labeling
Tuomas Launiainen, Keijo Heljanko, and Tommi Junttila: Efficient Model Checking of PSL Safety Properties
Tommi Junttila, and Petteri Kaski: Exact Cover via Satisfiability: An Empirical Study
Tero Laitinen, Tommi Junttila, and Ilkka Niemelä: Extending Clause Learning DPLL with Parity Reasoning
Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä: Partitioning SAT Instances for Distributed Solving
Matti Järvisalo, and Tommi Junttila: Limitations of restricted branching in clause learning
Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä: Incorporating Clause Learning in Grid-Based Randomized SAT Solving
Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä: Partitioning Search Spaces of a Randomized Search
Alessandro Cimatti, Jori Dubrovin, Tommi Junttila, and Marco Roveri: Structure-aware computation of predicate abstraction
Matti Järvisalo, and Tommi Junttila: On the Power of Top-Down Branching Heuristics
Jori Dubrovin, and Tommi Junttila: Symbolic model checking of hierarchical UML state machines
Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä: Incorporating Learning in Grid-Based Randomized SAT Solving
Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä: Strategies for Solving SAT in Grids by Randomized Search
Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä: Justification-Based Non-Clausal Local Search for SAT
Jori Dubrovin, Tommi Junttila, and Keijo Heljanko: Symbolic Step Encodings for Object Based Communicating State Machines
Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä: Justification-Based Local Search with Adaptive Noise Strategies
Tommi Junttila, and Jori Dubrovin: Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking
Tommi Junttila, and Petteri Kaski: Engineering an Efficient Canonical Labeling Tool for Large and Sparse Graphs
Matti Järvisalo, and Tommi Junttila: Limitations of Restricted Branching in Clause Learning
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Silvio Ranise, Peter van Rossum, and Roberto Sebastiani: Efficient theory combination via Boolean search
Armin Biere, Keijo Heljanko, Tommi Junttila, Timo Latvala, and Viktor Schuppan: Linear Encodings of Bounded LTL Model Checking
Keijo Heljanko, Tommi Junttila, Misa Keinänen, Martin Lange, and Timo Latvala: Bounded Model Checking for Weak Alternating Büchi Automata
Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä: A Distribution Method for Solving SAT in Grids
Armin Biere, Keijo Heljanko, Tommi Junttila, Timo Latvala, and Viktor Schuppan: Linear Encodings of Bounded LTL Model Checking
Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä: Unrestricted vs restricted cut in a tableau method for Boolean circuits
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
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Peter van Rossum, Stephan Schulz, and Roberto Sebastiani: The MathSAT 3 System
Keijo Heljanko, Tommi Junttila, and Timo Latvala: Incremental and Complete Bounded Model Checking for Full PLTL
Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi Junttila, Silvio Ranise, Peter van Rossum, and Roberto Sebastiani: Efficient Satisfiability Modulo Theories via Delayed Theory Combination
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
Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila: Simple Is Better: Efficient Bounded Model Checking for Past LTL
Tommi Junttila: New Orbit Algorithms for Data Symmetries
Tommi Junttila: New Canonical Representative Marking Algorithms for Place/Transition-Nets
Timo Latvala, Armin Biere, Keijo Heljanko, and Tommi Junttila: Simple Bounded LTL Model Checking
Matti Järvisalo, Tommi Junttila, and Ilkka Niemelä: Unrestricted vs Restricted Cut in a Tableau Method for Boolean Circuits
Tommi Junttila: Computational Complexity of the Place/Transition-Net Symmetry Reduction Method
Tommi Junttila, and Ilkka Niemelä: Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking
Tommi Junttila: Finding Symmetries of Algebraic System Nets
Program committee memberships ▼