bild
School of
Computer Science
and Communication
KTH / CSC / TCS

Degree project/exjobb project proposals at TCS

This page contains degree project proposals from members of the TCS group. If you have an idea of your own, or you don't find anything suitable on these pages you are welcome to get in touch with a member of faculty in the subject area you are interested in.

Project proposals i particular subject areas

Other project proposals

  • Railroad Timetabling
    Two possible master thesis, orignally from the group in optimization.
    More information: word-document.
    For further information contact PO Lindberg (polin@kth.se).
  • Formula Hardness and SAT Solving
    Given a logic formula, is it possible to set its variables in such a way that the formula is satisfied? This simple looking problem has been on centre stage in theoretical computer science ever since the field got started some 40 years ago, and was recently named as one of the Millennium Prize Problems comprising some of the major challenges for all of mathematics in the 21st century. Today, students of computer science worldwide learn in their introductory theory courses that this so-called SAT problem is what is known as NP-complete, and therefore is very, very hard in practice.
    Interestingly, practioners take a somewhat different view. During the last 10-15 years, SAT has developed from a problem of mainly theoretical interest into a practical approach for solving applied problems. Enormous progress in performance has led to satisfiability algorithms, so-called SAT solvers, becoming a standard tool for solving real-world problems with millions of variables in the context of, for example, hardware and software verification, electronic design automation, artificial intelligence, operations research, and bioinformatics. The theory of NP-completeness did not quite go away, however — for all these SAT solvers there are also known examples of tiny formulas with just a couple of hundred variables that make them fail miserably.
    How can modern SAT solvers be so good in practice? And how can one know for a particular formula whether it will be hard or easy? These are the kind of questions we want to study in these Master's thesis projects, using a mix of theoretical research and practical experiments.
    More information: html, pdf.
    Contact: Jakob Nordström.
  • Modular extraction of flow-graphs from Java bytecode
    Flow-graphs model software executions and are heavily used for formal verification of system correctness. We extract flow graphs from Java bytecode as part of our compositional technique of contol-flow software verification. We plan to make the extraction modular. Thus we could verify system before having its current implementation by exploiting information from interfaces. Moreover we plan to address the issue of exceptional flows, which are part of Java language and have high impact on a program control-flow.
    Project description: pdf
    Contact: Dilian Gurov, Pedro Gomes
  • Security monitor inlining in the ABS modelling language
    Project description: html, pdf
    Contact: Andreas Lundblad, Mads Dam
  • Previous projects

Get in touch with a member of faculty if you are interested in one of the projects above, if you have a project idea of your own, or if you wish to enquire about other projects ideas in a specific subject.

Published by: Mads Dam <mfd@nada.kth.se>
Updated 2015-01-27