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.)
Assoc. Prof., D.Sc. (Tech.)
Docent, D.Sc. (Tech.)
Docent, D.Sc. (Tech.)
Docent, D.Sc. (Tech.)
Dr.
Dr. Martin Gebser
Dr. Antonius Weinzierl
D.Sc. (Tech.) Jori Dubrovnik
D.Sc. (Tech.)
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.)
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: . Aalto University, Department of Information and Computer Science, 2014.
Tero Laitinen: . Aalto University, Department of Information and Computer Science, 2014.
Jori Dubrovin: . Aalto University, Department of Information and Computer Science, 2011.
Antti Hyvärinen: . 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: . Helsinki University of Technology, Faculty of Information and Natural Sciences, Department of Information and Computer Science, 2009.
Matti Järvisalo: . Helsinki University of Technology, Faculty of Information and Natural Sciences, Department of Information and Computer Science, 2008.
Emilia Oikarinen: . Helsinki University of Technology, Faculty of Information and Natural Sciences, Department of Information and Computer Science, 2008.
Misa Keinänen: . Helsinki University of Technology, Department of Computer Science and Engineering, 2006.
Heikki Tauriainen: . Helsinki University of Technology, Department of Computer Science and Engineering, 2006.
Toni Jussila: . Helsinki University of Technology, Department of Computer Science and Engineering, 2005.
Tommi Junttila: . Helsinki University of Technology, Department of Computer Science and Engineering, 2003.
Keijo Heljanko: . Doctoral Dissertation, Helsinki University of Technology, Department of Computer Science and Engineering, 2002.
Patrik Simons: . Helsinki University of Technology, Department of Computer Science and Engineering, 2000.
Tomi Janhunen: . Helsinki University of Technology, Department of Computer Science and Engineering, 1998.
Jussi Rintanen: . 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ä: . 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: . Helsinki University of Technology, Department of Computer Science and Engineering, 2007.
Emilia Oikarinen: . Helsinki University of Technology, Department of Computer Science and Engineering, 2006.
Misa Keinänen: . Helsinki University of Technology, Department of Computer Science and Engineering, 2005.
Tommi Syrjänen: . Helsinki University of Technology, Department of Computer Science and Engineering, 2003.
Heikki Tauriainen: . Helsinki University of Technology, Department of Computer Science and Engineering, 2003.
Toni Jussila: . Helsinki University of Technology, Department of Computer Science and Engineering, 2001
Keijo Heljanko: . Helsinki University of Technology, Department of Computer Science and Engineering, 1999
Patrik Simons: . Helsinki University of Technology, Department of Computer Science and Engineering, 1997
Tomi Janhunen: . Helsinki University of Technology, Department of Computer Science, 1994
Jussi Rintanen: . 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: . 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: . Helsinki University of Technology, Department of Engineering Physics and Mathematics, 2006.
Antti Hyvärinen: . Helsinki University of Technology, Department of Computer Science and Engineering, 2005.
Matti Järvisalo: . Helsinki University of Technology, Department of Computer Science and Engineering, 2004.
Emilia Oikarinen: . Helsinki University of Technology, Department of Engineering Physics and Mathematics, 2003.
(Received Helsinki University of Technology Master's Thesis award 2004)
Tuomo Pyhälä: . 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: . 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: . Helsinki University of Technology, Department of Computer Science and Engineering, 1999.
Patrik Simons: . Helsinki University of Technology, Department of Computer Science, 1995.
Tomi Janhunen: . Helsinki University of Technology, Department of Computer Science, 1993.
Jussi Rintanen: . 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 )
(COIN II), 01/2015-12/2017
(COIN I), 01/2012-12/2014
(StMcDes), 01/2009-12/2012
(MCM), 01/2008-12/2011
(MODSAFE), 02/2007-01/2011
(LIME2), 01/2009-9/2011
LightweIght formal Methods for distributed component-based Embedded systems (LIME), 10/2007-09/2009 ()
(SMUML), 01/2005-12/2007
(ACPT), 01/2005-12/2007
(WASP, Work Package 3), 9/2002-q9/2005
, 01/2002-12/2005
, 01/1998-12/2001
, 01/2001-12/2002
: a tool collection for answer-set programming.
: a tool collection for Boolean satisfiability.
: an smodels/perl program that solves sokoban levels (including a patch for ).
a deadlock and reachability checker which uses finite complete prefixes generated by the tool from 1-safe Petri nets and employes smodels as its computational engine.
: a bounded reachability checker based on process semantics.
: a bounded model checker for LTL.
: an LTL model checker using net unfoldings.
: a testing tool.
: 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.
: a benchmark generator based on factoring for SAT and ASP solvers.
: a testbench for implementations of algorithms for translating linear temporal logic (LTL) formulas into Büchi automata.