Prof. Ilkka Niemelä

Dr. Ilkka Niemelä

Professor of Computer Science, Dept. of Computer Science, School of Science, Aalto University
Currently serving as Provost of Aalto University

Contact info for the Provost position:

Postal Address: Aalto University
P.0.Box 17800, FI-00076 AALTO, Finland

Street address: Lämpömiehenkuja 2, Aalto Otaniemi campus, Espoo

Email: provostaalto.fi

Appointments: Contact
Executive Assistant
Pia Holmberg
pia.holmbergaalto.fi, + 358 40 542 1546

[Papers] [Research] [Software] [Tutorials] [Teaching] [Conferences]

Brief Biography
Tiivistelmä virkaanastujaisesitelmästä 19.9.2000: Laskennallinen logiikka - soveltavaa tietojenkäsittelyteoriaa
(Summary of the inauguration talk Sep 19, 2000: Computational logic - applied theoretical computer science; in Finnish)
Scientific Positions of Trust
- EurAI Fellow
- Member of the Finnish Academy of Science and Letters
- Member of the Finnish Academy of Technology
- Editor-in-Chief of Theory and Practice of Logic Programming published by Cambridge University Press (2010-2014)
- Editorial board member of Journal of Artificial Intelligence Research (2005-2011)
- Member of the Executive Committee of the Association for Logic Programming (ALP) (2005-2009)
- Steering Committee Member of the International Workshops on Nonmonotonic Reasoning
- Steering Committee Member of the International Conferences on Logic Programming and Nonmonotonic Reasoning
- Steering Committee Member of the European Conference on Logics in Artificial Intelligence (JELIA)
- Steering Committee Member of the ESF Research Networking Program on Games for Design and Verification (GAMES)
- Management Committee Member of the COST Action IC0901: Rich-Model Toolkit - An Infrastructure for Reliable Computer System

Papers

Research

Head of the Computational Logic Group in the Department of Computer Science
One of the Principal Investigators of the Finnish Centre of Excellence in Computational Inference Research (COIN)
Research interests
- knowledge representation, default reasoning, logic programming
- automated reasoning, satisfiability checking, constraint satisfaction
- computer-aided verification, symbolic model checking, automated testing
- computational complexity
Projects
- LightweIght formal Methods for distributed component-based Embedded systems (LIME2) 2009-2011
- Symbolic Testing and Model Checking of Distributed Embedded Systems (StMcDes) 2009-2012
- Methods for Constructing and Solving Large Constraint Models (MCM) 2008-2011
- LightweIght formal Methods for distributed component-based Embedded systems (LIME) 2007-2009 (publications)
- Model-Based Safety Evaluation of Automation Systems (MODSAFE) 2007-2011
- Symbolic Methods for UML Behavioural Diagrams (SMUML) 2005-2007
- Advanced Constraint Programming Techniques for Large Structured Problems (ACPT) 2005-2007
- Working group on Answer Set Semantics (The Computational Logic group is the leader of Work package 3: Language Extensions and Software Engineering for ASP )
- Applications of Rule-Based Constraint Programming 2002-2005
- Formal Methods in Distributed Systems 2000-2002
- Constraint Programming Based on Default Rules 1998-2001
- Conformance Testing and Bounded Model Checking 2002
- Analysis and Development of Cryptosystems 2001-2005
- Security in Mobile Ad-hoc Networks, 2001

Software

lp2diff, a translator mapping logic programs to SMT theories implemented by Tomi Janhunen.
Smodels, a system for rule-based constraint programming based on logic programs with the stable model semantics implemented in C++.
GnT, an implementation of disjunctive stable models on top of Smodels. Note that this can compute also, e.g., minimal models of sets of clauses.
BCSat - an implementation of a tableau method for Boolean circuit satisfiability checking done by Tommi Junttila.
Test case generation for minimal model and other propositional reasoners.
An Eclipse Prolog implementation of a tableau-based method for automating circumscriptive reasoning (TABLEAUX'96, ECAI'96).

Tutorials and short courses given

Answer Set Programming. An invited tutorial given at the 19th European Conference on Artificial Intelligence (ECAI 2010), August 16-20, Lisbon, Portugal. (Slides [pdf]).
The Implementation of Answer Set Solvers. An invited tutorial given at the 20th International Conference on Logic Programming (ICLP'04), September 6-10, 2004, Saint-Malo, France (Slides [ps.gz]).
Answer-Set Programming: a Declarative Knowledge Representation Paradigm. A tutorial given at the 13th European Summer School in Logic, Language and Information (ESSLLI-2001), Helsinki, Finland, August 13-24, 2001 together with Mirek Truszczynski. (Handout, Slides).
Practical Tools for Knowledge Representation and Nonmonotonic Reasoning. A tutorial given at the 17th National Conference on Artificial Intelligence, Austin, Texas, July 30-August 3, 2000 together with Mirek Truszczynski. (Handout, Slides ).
Stable Model Semantics: From Theory to Implementations and Applications. An invited tutorial given at the First International Conference on Computational Logic (CL2000), Imperial College, London, UK, July 24-28, 2000 (Handout, Slides ).
Smodels: a System for Answer Set Programming, Dresden University of Technology, Department of Computer Science, Dresden, Germany, June 5--7, 2000. (Short course)
Default Logic: From Theory to Applications. A course given at the 11th European Summer School in Logic, Language and Information , Utrecht University, Aug 16-20, 1999.
Proof Systems for Nonmonotonic Logics. A tutorial given at the 12th International Conference on Automated Deduction, Nancy, France, June 28-July 1, 1994 together with Camilla Schwind. (Lecture Notes)

Teaching

T-79.5103 Computational Complexity Theory. This is an advanced course on computational complexity covering topics such as NP-completeness, randomized algorithms, cryptography, approximation algorithms, parallel algorithms, polynomial hierarchy, PSPACE-completeness.
T-79.5104 Advanced Course in Computational Logic. This is an advanced course on logic and its applications in computer science and engineering. Subjects covered: modal logics (syntax, semantics, proof theory and computational properties) and Current applications in computer science and engineering.
T-79.4101 Discrete Models and Search . The course provides an introduction to the fundamental concepts, techniques and tools used in dealing with large, weakly structured combinatorial search spaces. The topics covered include: Search spaces and search methods. Backtracking, local and heuristic search. Representing and solving search problems using propositional satisfiability, constraint programming and integer programming techniques.
T-79.4202 Principles of Algorithmic Techniques . Fundamental algorithm design paradigms: divide-and-conquer, greedy algorithms, dynamic programming. Randomised algorithms. Introduction to the analysis of algorithms and the theory of NP-completeness.
T-79.7001 Postgraduate Course in Theoretical Computer Science, Spring 2010 .
T-79.4001 Seminar on Theoretical Computer Science . This is a seminar course covering current research topics in theoretical computer science. The topic varies yearly.
T-79.298: Postgraduate Course in Digital Systems Science, 2001 .
Tik-79.144 Logic in Computer Science: Foundations, Spring 1997. This is an introductory course on logic and its applications in computer science. Subjects covered are: propositional and predicate logic, model theory, proof theory, semantic/analytic tableaux, resolution.
Tik-79.154 Logic in Computer Science: Special Topics II, Autumn 1997. This is an advanced course on logic and its applications in computer science and engineering. Subjects covered in 1997 are: advanced decision methods for propositional logic (Davis-Putnam, BDDs, stochastic methods) and for rule-based reasoning.
Tik-79.230 Foundations of Agent-Based Computing, Spring 1998. This is a course on architectures, implementation technology and applications of agent-based systems.