Computational Logic
The Computational Logic Group develops automated reasoning techniques for solving challenging computational problems in engineering and science. The current focus is on efficient computational methods for solving large constraint satisfaction problems formally represented as Boolean satisfiability (SAT) problems or their generalizations, or expressed in terms of rule-based constraints used in answer-set programming (ASP). The group has a strong track record in research on verification and testing of automation systems and software, as well as applying formal methods in the analysis of distributed systems.
Prof. Ilkka Niemelä, the head of the group (on leave from professorship)
Docent, D.Sc. (Tech.) Tommi Junttila
Assoc. Prof., D.Sc. (Tech.) Keijo Heljanko
Docent, D.Sc. (Tech.) Tomi Janhunen
Docent, D.Sc. (Tech.) Matti Järvisalo
Docent, D.Sc. (Tech.) Jussi Rintanen
Dr. Bart Bogaerts
Dr. Martin Gebser
Dr. Antonius Weinzierl
D.Sc. (Tech.) Jori Dubrovnik
D.Sc. (Tech.) Antti Hyvärinen
D.Sc. (Tech.) Toni Jussila
D.Sc. (Tech.) Misa Keinänen
D.Sc. (Tech.) Roland Kindermann
D.Sc. (Tech.) Tero Laitinen
PhD Guohua Liu
D.Sc. (Tech.) Emilia Oikarinen
D.Sc. (Tech.) Patrik Simons
D.Sc. (Tech.) Tommi Syrjänen
D.Sc. (Tech.) Heikki Tauriainen
Lic.Sc. (Tech.) Vesa Luukkala
M.Sc. (Tech.) Rehan Aziz
M.Sc. (Tech.) Juho Frits
M.Sc. (Tech.) Laura Koponen
M.Sc. (Tech.) Matti Koskimies
M.Sc. (Tech.) Lea Kylmälä
M.Sc. (Tech.) Kari Kähkönen
M.Sc. (Tech.) Jussi Lahtinen
M.Sc. (Tech.) Jori Bomanson
M.Sc. (Tech.) Markku Riekkinen
M.Sc. (Tech.) Jani Lampinen
M.Sc. (Tech.) Mai Nguyen
M.Sc. (Tech.) Janne Nykopp
M.Sc. (Tech.) Vesa Ojala
M.Sc. (Tech.) Binda Pandey
M.Sc. (Tech.) Tuomo Pyhälä
B.Sc. Teemu Hankala
Stud.Tech. Janne Kauttio
Stud.Tech. Unto Kuuranne
Stud.Tech. Sami Liedes
Stud.Tech. Leo Moisio
Stud.Tech. Teemu Pudas
Stud.Tech. Jukka Pajunen
Stud.Tech. Roosa Piitulainen
Roland Kindermann: SMT-based Verification of Timed Systems. Aalto University, Department of Information and Computer Science, 2014.
Tero Laitinen: Extending SAT Solver with Parity Reasoning. Aalto University, Department of Information and Computer Science, 2014.
Jori Dubrovin: Efficient Symbolic Model Checking of Concurrent Systems. Aalto University, Department of Information and Computer Science, 2011.
Antti Hyvärinen: Grid Based Propositional Satisfiability Solving. Aalto University, Department of Information and Computer Science, 2011.
(Received one of the best doctoral dissertation awards of Aalto University School of Science in 2011.)
Tommi Syrjänen: Logic Programs and Cardinality Constraints: Theory and Practice. Helsinki University of Technology, Faculty of Information and Natural Sciences, Department of Information and Computer Science, 2009.
Matti Järvisalo: Structure-Based Satisfiability Checking: Analyzing and Harnessing the Potential. Helsinki University of Technology, Faculty of Information and Natural Sciences, Department of Information and Computer Science, 2008.
Emilia Oikarinen: Modularity in Answer Set Programs. Helsinki University of Technology, Faculty of Information and Natural Sciences, Department of Information and Computer Science, 2008.
Misa Keinänen: Techniques for Solving Boolean Equation Systems. Helsinki University of Technology, Department of Computer Science and Engineering, 2006.
Heikki Tauriainen: Automata and Linear Temporal Logic: Translations with Transition-Based Acceptance. Helsinki University of Technology, Department of Computer Science and Engineering, 2006.
Toni Jussila: On Bounded Model Checking of Asynchronous Systems. Helsinki University of Technology, Department of Computer Science and Engineering, 2005.
Tommi Junttila: On the Symmetry Reduction Method for Petri Nets and Similar Formalisms. Helsinki University of Technology, Department of Computer Science and Engineering, 2003.
Keijo Heljanko: Combining Symbolic and Partial Order Methods for Model Checking 1-Safe Petri Nets. Doctoral Dissertation, Helsinki University of Technology, Department of Computer Science and Engineering, 2002.
Patrik Simons: Extending and Implementing the Stable Model Semantics. Helsinki University of Technology, Department of Computer Science and Engineering, 2000.
Tomi Janhunen: Non-Monotonic Systems: A Framework for Analyzing Semantics and Structural Properties of Non-Monotonic Reasoning. Helsinki University of Technology, Department of Computer Science and Engineering, 1998.
Jussi Rintanen: Lexicographic Ordering as a Basis for Priorities in Default Reasoning. Helsinki University of Technology, Department of Computer Science and Engineering, 1997.
(Received the Finnish Science Academy stipendium for a distinguished doctoral thesis in 1997)
Ilkka Niemelä: Autoepistemic Logic as a Unified Basis for Nonmonotonic Reasoning. Helsinki University of Technology, Department of Computer Science, 1993.
(Received the annual dissertation award of the Finnish Society for Computer Science for a distinguished doctoral dissertation in Computer Science.)
Vesa Luukkala: Rule-based Metaprogramming for Smart Spaces. Aalto Unversity, Department of Computer Science, 2015.
Antti E.J. Hyvärinen: Approaches to Grid-Based SAT Solving. Helsinki University of Technology, Department of Information and Computer Science, 2009.
Matti Järvisalo: Impact of Restricted Branching on Clause Learning SAT solving. Helsinki University of Technology, Department of Computer Science and Engineering, 2007.
Emilia Oikarinen: Modular Answer Set Programming. Helsinki University of Technology, Department of Computer Science and Engineering, 2006.
Misa Keinänen: Solving Boolean Equation Systems. Helsinki University of Technology, Department of Computer Science and Engineering, 2005.
Tommi Syrjänen: Logic Programming with Cardinality Constraints . Helsinki University of Technology, Department of Computer Science and Engineering, 2003.
Heikki Tauriainen: On Translating Linear Temporal Logic into Alternating and Nondeterministic Automata. Helsinki University of Technology, Department of Computer Science and Engineering, 2003.
Toni Jussila: Bounded Model Checking for Verifying Concurrent Programs. Helsinki University of Technology, Department of Computer Science and Engineering, 2001
Keijo Heljanko: Deadlock and Reachability Checking with Finite Complete Prefixes. Helsinki University of Technology, Department of Computer Science and Engineering, 1999
Patrik Simons: Towards Constraint Satisfaction through Logic Programs and the Stable Model Semantics. Helsinki University of Technology, Department of Computer Science and Engineering, 1997
Tomi Janhunen: Investigations on Cautious Autoepistemic Reasoning . Helsinki University of Technology, Department of Computer Science, 1994
Jussi Rintanen: Priorities and Nonmonotonic Reasoning. Helsinki University of Technology, Department of Computer Science, 1993
Markku Riekkinen: Integrating Stratum and A+ Functionalities in Moodle: Architecture and Evaluation. Aalto University, Department of Computer Science, 2016.
Binda Pandey: Adaptive Learning for Mobile Network Management. Aalto University, Department of Computer Science, 2016.
Evgenia Antonova: Applying Answer Set Programming in Game Level Design. Aalto University, Department of Computer Science, 2015.
Weiming Wu: Design and Implementation of a Shared Task Queue Groupware. Aalto University, Department of Computer Science, 2015.
Laura Koponen: Constraint-Based Optimization of Phylogenetic Supertrees. Aalto University, Department of Computer Science, 2015.
Jori Bomanson: Developing Efficient Encodings for Weighted Expressions in Answer Set Programs. Aalto University, Department of Information and Computer Science, 2014.
Tao Sun: Parameter Selection in Translation-Based Approaches to Answer Set Solving. Aalto University, Department of Information and Computer Science, 2012.
Mai Nguyen: Preferential Optimization of University Students' Timetables. Aalto University, Department of Information and Computer Science, 2012.
Rehan Abdul Aziz: Distributed Rule-Based Resource Allocation in Smart Spaces. Aalto University, Department of Information and Computer Science, 2011.
Tero Laitinen: Extending SAT Solver with Parity Constraints. Aalto University, Department of Information and Computer Science, 2010.
Juho Frits: Model Checking Embedded Control Software. Aalto University, Department of Information and Computer Science, 2010
Lea Kylmälä: University Timetabling Using Answer Set Programming Techniques. Aalto University, Department of Information and Computer Science, 2010.
Vesa Ojala: Counterexample analysis for automated refinement of data abstracted state machine models. Helsinki University of Technology, Department of Information and Computer Science, 2008.
Kari Kähkönen: Automated dynamic test generation for sequential Java programs. Helsinki University of Technology, Department of Information and Computer Science, 2008.
Jussi Lahtinen: Model checking timed safety instrumented systems. Helsinki University of Technology, Department of Information and Computer Science, 2008.
Jani Lampinen: Interface specification methods for software components. Helsinki University of Technology, Department of Information and Computer Science, 2008.
Matti Koskimies: Applying model checking to analysing safety instrumented systems. Helsinki University of Technology, Department of Information and Computer Science, 2008.
Jori Dubrovin: Jumbala - an action language for UML state machines. Helsinki University of Technology, Department of Engineering Physics and Mathematics, 2006.
Antti Hyvärinen: SATU: A system for distributed propositional satisfiability checking in computational GRIDs. Helsinki University of Technology, Department of Computer Science and Engineering, 2005.
Matti Järvisalo: Proof complexity of cut-based tableaux for Boolean circuit satisfiability checking. Helsinki University of Technology, Department of Computer Science and Engineering, 2004.
Emilia Oikarinen: Testing the equivalence of disjunctive logic programs. Helsinki University of Technology, Department of Engineering Physics and Mathematics, 2003.
(Received Helsinki University of Technology Master's Thesis award 2004)
Tuomo Pyhälä: Specification-Based Test Selection in Formal Conformance Testing. Helsinki University of Technology, Department of Computer Science and Engineering, 2003.
Rauni Pääkkönen: Implementing a formal agent description language. Helsinki University of Technology, Department of Computer Science and Engineering, 2001.
Heikki Tauriainen: Automated testing of Büchi automata translators for linear temporal logic. Helsinki University of Technology, Department of Computer Science and Engineering, 2000.
( Received the annual award of the Finnish Society for Computer Science for a distinguished Master's Thesis in Computer Science )
Tommi Syrjänen: A Rule-Based Formal Model for Software Configuration. Helsinki University of Technology, Department of Computer Science and Engineering, 1999.
Patrik Simons: Efficient Implementation of the Stable Model Semantics for Normal Logic Programs. Helsinki University of Technology, Department of Computer Science, 1995.
Tomi Janhunen: Weakened Negative Introspection in Autoepistemic Reasoning. Helsinki University of Technology, Department of Computer Science, 1993.
Jussi Rintanen: Stratification and Tractability in Nonmonotonic Reasoning. Helsinki University of Technology, Department of Computer Science, 1992.
( Received the annual award of the Finnish Society for Computer Science for a distinguished Master's Thesis in Computer Science )
Finnish Centre of Excellence in Computational Inference Research (COIN II), 01/2015-12/2017
Finnish Centre of Excellence in Computational Inference Research (COIN I), 01/2012-12/2014
Symbolic Testing and Model Checking of Distributed Embedded Systems (StMcDes), 01/2009-12/2012
Methods for Constructing and Solving Large Constraint Models (MCM), 01/2008-12/2011
Model-Based Safety Evaluation of Automation Systems (MODSAFE), 02/2007-01/2011
LightweIght formal Methods for distributed component-based Embedded systems (LIME2), 01/2009-9/2011
LightweIght formal Methods for distributed component-based Embedded systems (LIME), 10/2007-09/2009 (publications)
Symbolic Methods for UML Behavioural Diagrams (SMUML), 01/2005-12/2007
Advanced Constraint Programming Techniques for Large Structured Problems (ACPT), 01/2005-12/2007
Working group on Answer Set Semantics (WASP, Work Package 3), 9/2002-q9/2005
Applications of Rule-Based Constraint Programming, 01/2002-12/2005
Constraint Programming Based on Default Rules, 01/1998-12/2001
Conformance Testing and Bounded Model Checking, 01/2001-12/2002
ASPTOOLS: a tool collection for answer-set programming.
SATTOOLS: a tool collection for Boolean satisfiability.
SSOKOBAN: an smodels/perl program that solves sokoban levels (including a patch for xsokoban).
MCSMODELS a deadlock and reachability checker which uses finite complete prefixes generated by the PEP tool from 1-safe Petri nets and employes smodels as its computational engine.
PUNROLL: a bounded reachability checker based on process semantics.
BOUNDSMODELS: a bounded model checker for LTL.
UNFSMODELS: an LTL model checker using net unfoldings.
BOMOTEST: a testing tool.
BCSAT: an implementation of a tableau method for Boolean circuit satisfiability checking. The file format for Boolean circuits and a translator from Boolean circuits to CNF is also available.
GENFACBM: a benchmark generator based on factoring for SAT and ASP solvers.
LBTT: a testbench for implementations of algorithms for translating linear temporal logic (LTL) formulas into Büchi automata.
- Published:
- Updated: