Cristian Prisacariuhome
research
projects
publications
master topics
teaching
personal
NEWS
The first female mathematician to receive the prestigious Fields Medal is Maryam Mirzakhani from Stanford University. Mirzakhani said: "I will be happy if it encourages young female scientists and mathematicians. I am sure there will be many more women winning this kind of award in coming years." Mirzakhani was born and raised in Tehran, where as a young girl she dreamed of becoming a writer. By high school, however, her affinity for solving mathematical problems and working on proofs had shifted her sights.

The Kavli Week is celebrating the Kavli Prize with Ceremony Show, Popular science lectures, and academic symposia and lectures by the prize winners. A lot of money are involved, partly sponsored by the Fred Kavli Foundation.

Heidelberg Laureate Forum - Abel, Fields and Turing Laureates Meet the Next Generation. Winners of the prestigious Abel Prize, Fields Medal and Turing Award will meet ambitious young scientists starting with 23-27 September 2013.

The Abel Prize in mathematics (with value ~1Mil $) is given this year on 22 May 2012 to Endre Szemeredi, a Hungarian mathematician who worked, among other, in the fields of combinatorics and theoretical computer science.

DEON 2012 - 11th International Conference on Deontic Logic in Computer Science, is held during 16-18 July 2012, at University of Bergen, Norway. Submission deadline is 5 March.

Noam Chomsky in Oslo, two days on 5-6 September, 2011. Come on 5th from 16:15-18 in Sophus Lies auditorium in Blindern campus to hear "The machine, the ghost, and the limits of understanding: Newtons contributions to the study of mind"; and on 6th from 19:00 in Storsalen (the big room) in Chateau Neuf right near Majorstuen T-station to hear about "Changing contours of world order".

Master Topics

contact

Contents

1  General Concerns

Contact: Christian Johansen; office: room 8166 in OJD building; e-mail: cristi@ifi.uio.no.

The projects listed here are of varying difficulty, but all have minimal requirements which, if satisfied, give one a Master level thesis. This page contains only short descriptions, with some more details given in some cases. For full length description one needs to contact me (at the office or through e-mail). Many of the projects have alternative supervisors; those persons can also be contacted related to the particular project and supervision.

Since all these projects and ideas are on-line (some sitting here for quite some time now) it may be that someone else out there has already started working on them, individually, or already has finished with a nice solution. If any of you know of such solutions please e-mail me about them, sending links and information about the person/place and specific thesis project that you refer to. I am always interested to know of alternative solutions/projects to the ones listed here.

Many of these projects, if finished in a good way, can become startup companies headed by you, possibly in conjunction with a company like Inven2.

Many of the topics are flexible and related to other topics. In consequence, it can be possible that two or more people work on a topic or collaborate between related topics. For such collaborative approaches we need to discuss the possibilities.

If you have any other ideas for doing a master project (or PhD thesis) with me then just send me an e-mail.

For more/other projects send a request through e-mail.

For some of the projects there are different extra possibilities, like to travel, e.g., as exchange student in some EU university or to related international events like summer schools; or to take up summer-jobs, or part-time positions. These opportunities are signalled for each topic by a respective icon:

  • Summer-jobs: are usually taken in between the study years, during the summer period, and can be in the form of 100% employment. The company decides based on the situation and the student. A MSc topic in this category signals such a possibility.
  • Part-time jobs: We usually encourage students and companies to consider only a 20% employment, so that it does not interfere much with the study program. But this is not a strict requirement, and cannot be enforced in any way. Moreover, it depends on the student and the situation.
  • Travelling: is usually done as either stays abroad for a short period of time (1 - 6 months) to another EU university which we have collaboration with; or very short travels to summer schools (when appropriate).

2  Formal Tools for Security, Parallelism, and Networking

The topics in this section are part of the recent ConSeRNS team that was formed at IFI with the purpose to combine competences on security, concurrency and parallelism, and resilient networks, also focusing on the integration of the human in such systems. The competences of ConSeRNS can be seen useful for analyzing formally the security properties of complex systems. The same competences can be useful for future complex systems such as ubiquitous systems where networking and communication, as well as parallel and distributed computation are extremely central, and the human aspect imposes strict safety and security concerns.

These topics are about formal tools that can be used to analyze and build systems in various forms. These tools are of industrial quality and many of them have reached a learning level that can easily be taken by a master student from IFI. Some tools are used to analyze systems to ensure lack of errors. Other tools can be used to generate code. Whereas other tools can be used to obtain quantitative and qualitative information about a system, like what is the expected uptime of this server. The tools can be used for systems from real-life, as well as software systems, security protocols, networking, multi-processor, supercomputer, or distributed systems, etc.

Each topic has as focus one such tool. The goal is to learn the tool and to apply it to a real-life case study.

SPIN the bugs

up to top
Short description:
If interested in guaranteeing the absence of errors in programs or systems, then you should try the SPIN tool. SPIN is extensively used in industry and academia, with at least one book written about it. For this topic, the student has to learn to use SPIN and to apply SPIN on a case study system coming from a real-life problem. The case studies will come from the industrial contacts we have, e.g., in the oil, transportation, networking, government, health, software.
Alternative supervisors: Christian Johansen, Olaf Owe, Martin Steffen
Read more details ...
SPIN is a model checking tool that is used to define properties and then check these against the system/model that the developer is interested in. When a property is not satisfied, then the presence of the bug is explicitly reported by SPIN. When a property is deemed by SPIN to hold for the system, then we can have complete confidence. (reed this introductory paper)

As learning outcomes, the student will gain good knowledge of the SPIN tool and will be ready to use it in various industrial settings where more complex systems are built (which is the case in many industrial products, e.g., coming from aerospace, automotive, oil, or software industries). The student will also gain a basic understanding of how to model systems and software, and how to specify requirements and properties of such systems. Modeling and specifications are a crucial part of software architecture which helps reduce the overall costs of building a system. Modeling is now becoming the state-of-the-art in building software systems, starting from a model and generating the end code. It is our belief that modeling will be a future way of developing complex software.

Because of the large community around SPIN, the student will most likely have an interesting/lively experience with this tool.

Master of Ceremonies

up to top
Short description:
You are interested in security protocols. Ceremonies [12, 32] are a new view which extends security protocols by integrating the human factor in the picture, as well as looking at the security protocol/system in entirety, making the assumptions explicit and composing several protocols for communication and security in the same analyses.

There are very few tools and formalisms for ceremonies, therefore you will have a lot of freedom. You will investigate and build a tool for ceremonies based on an existing tool for security protocols. You will investigate graphical languages and code generation, or you can look into how to analyze ceremonies.

Alternative supervisors: Christian Johansen, Olaf Owe, Audun Jøsang
Read more details ...
As learning outcomes, the student will work with a tool for security protocols, extending it to security ceremonies. This knowledge can readily be used in industry afterwards, for modeling, analyzing, and building complex security systems. The case studies of security ceremonies will come from a real-life industry system, which will give good contacts and experience to the student.

The student should have ability to program and to work with a new tool (i.e., install, compile, and use a new tool environment, most probably on a Linux machine, because this is where many of the tools are natively running).

Or you are interested in sociology, then this topic could fit you well, and allow you to work with actor network theory or analyze the social [6] and cognitive aspects [34] of the humans involve. A famous quote is most explanatory: Bruce Schneier said "Security is fundamentally not a technology problem, but a people’s problem."

Be a JavaSPI

up to top
Short description:
This project is for someone interested in security protocols and Java programming. The framework JavaSPI is used to generate Java implementations for security protocols specified in the SPI language. (see this paper describing JavaSPI) Languages for modelling and specification of security protocols will be an important learning part of this project. The tool is to be applied to a case study taken from the OffPAD project or from Thales AS.
Alternative supervisors: Christian Johansen, Martin Steffen, Audun Jøsang
Read more details ...
As learning outcomes, the student will become familiar with languages for specifying security protocols like SPI which is similar to what are called process calculi. Such languages are wide spread and several other tools for security use them, like the AVISPA or the FDR3 from Oxford. Therefore, working with SPI would open the student to any other similar languages which may be encountered later in the career (these are used also for modelling distributed systems, concurrent processes, etc.).

I QP-nano forever

up to top
Short description:
You are interested in programming wireless sensors networks and embedded systems. You will use a different approach, based on modeling and automatic code generation. The tool that will be used is the QP-nano. This is specially designed for resource constrained systems. The tool is part of a tool suite coming from QuantumLeaps and has also a book written about it, which the student will study.
Alternative supervisors: Christian Johansen, Olaf Owe, Frank Eliassen
Read more details ...
As learning outcomes, the student will gain knowledge with the QP tool framework, in particular with the QP-nano for wireless sensors and embedded systems. One would learn how to develop systems by modeling and generating the implementation code. The modeling is done using a graphical language. This is highly attractive for industry people, both because of the visual language and because of the code generation. Even more, the model can be used for verification purposes, which is highly desired for safety-critical systems, e.g., as those that DNV or Thales is working with.

iSAT in one year

up to top
Short description:
Train controllers, atomic reactors, or flight stabilizers, can be modeled with iSAT so to check their safety critical properties. iSAT3 comes from a long line of tools for hybrid systems built in Germany in collaboration with many international partners. You have to learn to use iSAT on a problem from rail transportation or from oil industry.
Alternative supervisors: Christian Johansen, Olaf Owe, Martin Steffen
Read more details ...
As learning outcomes, the student will gain knowledge with the iSAT tool and its modeling methodology. This is based on satisfiability for logics and encoding hybrid systems as logic formulas for doing bounded model checking. One has to go through several of the existing earlier case studies done with iSAT (e.g., iSAT was successfully used for investigating a new European Train Controlling System). In the second phase one will model a new case study with iSAT and check properties.

Such knowledge will be highly attractive for industry, both because of the modeling power that iSAT has and because of the kind of critical systems that iSAT can handle, which become more prevalent in various areas like oil, avionics, automotive, eHospital, etc.

Because of the community around iSAT, the student will most likely have an interesting/lively experience with this tool.

Java PathFinder

up to top
Short description:
Interested in developing Java safety-critical systems, on which lives or money depend? Then you better make sure that you do not leave bugs behind. One way to make sure is by using Java PathFinder. This is a model checking tool from the NASA Ames Research Center that has been developed over almost ten years and used in many industry projects, as well as during the Google Summer of Code. You will have to learn to use JPF and to work on a case study from industry, trying to show the absence of certain kinds of bugs.
Alternative supervisors: Christian Johansen, Olaf Owe, Volker Stolz
Read more details ...
As learning outcomes, the student will become familiar with the Java PathFinder tool and will learn how to show the absence of bugs in a Java program. This is different than the common “debugging”, which just runs the program and looks for obvious malfunctions. With Java PathFinder one has certainty that the specified kind of bugs are not present in the respective Java application.

The case study comes from an existing Java application, like for example the Jitsi implementation or the OTR messaging system. The case study can very well be related to the annual events around JPF, like the GSoC or the Ames workshops.

Because of the lively community around JPF, the student will most likely have an interesting experience with this tool. It is also possible to travel as exchange students to external institutes where JPF is used.

Kerberos – good, bad, or ugly?

up to top
Short description:
If you are interested in security then this project is about a widely used security protocol; precisely the Kerberos authentication protocol. You will investigate closely this complex protocol and if possible an open-source implementation of it. The work will be based on existing analyses that have already been carried out for parts of the protocol, of simplifications of it, like done in this work. You will have opportunity to use tools for modelling and analysing such security protocols. One recent powerful tool (but also not so easy to tame) is the CryptoVerif that was already used successfully by the INRIA Paris group on parts of Kerberos. But many other tools exist (e.g.: ProVerif or Murphi), and the exactly which to use will be decided together with the student. Alternatively, this topic can also evolve in a (critical) “how-to” manual.
Alternative supervisors: Christian Johansen, Audun Jøsang, Martin Steffen
Read more details ...
As learning outcomes, the student will gain knowledge of one of the most used authentication protocols in practice. A start for the thesis study can be this good tutorial on Kerberos as well as the official MIT documentation page. The Kerberos community is lively and sponsored by some of the major players in the field. The official documentation is a IETF standard RFC-1510.

3  With Industry Cooperation

The topics in this category involve collaboration with an industry partner. Collaboration can vary: from internships, to interactions with the company staff on matters related to the project, to taking up case studies of practical application to the specific company.

Companies actively involved in the master projects below are:

  • Tellu AS : developing cloud services for monitoring devices, usually with applications in health and ambient assisted living, but also in security, transportation, and endurance sports, among others.
  • Anacon AS : working on designs of railway infrastructures such as high-speed tracks or full railway stations.
  • Karde AS : working on user-oriented solutions for elderly and disabled people.

Other possible industry involvement can be with the following companies and institutions. The specifics depend on the project and the student, and are to be decided during the master project work.

  • Thales, DNV, Statoil, IFE, SINTEF, NR, Simula

RedHat’s JBoss Drools and RuleML

up to top
Short description:
Interested in Expert Systems ? Then Drools (and the other JBoss components) are what you need to know in order to be able to build expert systems. Knowledge of Java is needed, because Drools is build on the Java Beans. Drools is a Rules Engine (among other things) and has its own rules description language. But the standard is RuleML (i.e., rules markup language).

You will have to build a translation tool from RuleML into the DRL input language of Drools.

You will be spending time in the Tellu company, which has Drools at the core of their products. You will most probably interact with the RedHat community around Drools if your translation is to be integrated in future Drools releases.

Alternative supervisors: Christian Johansen, Olaf Owe, Tellu AS
Read more details ...
As learning outcomes, the student will become familiar with RedHat’s JBoss Drools engine and will know how to write rules in the DRL input language of Drools. Thus, by the end of the master studies, the student will have basic knowledge of rule-based programming. The student will learn RuleML language, and the expressive features it has. Moreover, the student will gain knowledge of XML languages and related technologies like XSLT for translating XML-based languages into other languages.

The practical part of the topic is to implement a translation tool from RuleML into DRL. This implementation can be done in various ways, raging from a XSLT processor, which could be used as a preprocessor providing input to Drools, or a Java package, which could be used directly inside Drools. This practical side is desired by the Drools community, as no such automatic translation exists, and the RuleML is a language with a good user community, which would like to benefit from the power of the Drools engine for running their existing expert systems specifications.

The student will take a case study coming from one of Tellu’s existing applications. This means this application will have to be re-written by the student in RuleML and used to test the translator software.

The student could, depending on the will, interact with the RedHat community around Drools in order to get the translator in the main Drools releases. Most probably, the student will interact with the friendly RuleML community when learning the various features of RuleML, so to see how much (which dialects) of RuleML will the translator handle. For rule engines and rule-based programming, Tellu can provide the necessary interaction; and the student may spend time (internship) in the company.

Parallel Drools – parallelization for the popular declarative rule engine from RedHat JBoss

up to top
Short description:
Interested in parallelism to give more power to Expert Systems ? The Drools engine (and the other JBoss components) could benefit greatly from a thorough study into possible ways of parallelization. Knowledge of Java is needed, because Drools is build on the Java Beans. Drools is a Rules Engine (among other things) developed by the RedHat community which is very much concerned with speed and optimization of their projects. But parallelization is not so obvious for rule engines.

The student will investigate Java threads and parallelization mechanisms that could be used for Drools, as well as the existing solutions put in place by the RedHat team.

You may be spending time in the Tellu company, which has Drools at the core of their products and are interested in speeding up their products.

Alternative supervisors: Christian Johansen, Martin Steffen, Tellu AS
Read more details ...
As learning outcomes, the student will become familiar with RedHat’s JBoss Drools engine and will know how to write rules in the DRL input language of Drools. Thus, by the end of the master studies, the student will have basic knowledge of rule-based programming. The student will become expert in thread-based parallel programming, in the Java style. Moreover, the student will gain experience with contributing to a large scale software project maintained by an open-source community.

The practical part of the topic is work with the Drools Java-based rule engine and programming environment, and at the same time will involve working with the thread-based parallel programming approach that Java provides. In particular, parts of the Drools engine are not thread-safe. The student will focus on these parts, and investigate if and how they can be made thread-safe, or in which situation they can be used in a threaded environment.

The student will take a case study coming from one of Tellu’s existing applications.

For rule engines and rule-based programming, Tellu can provide the necessary interaction; and the student may spend time (internship) in the company. For parallel programming and thread-safety, the PMA group is a good place.

Trains iSAT

up to top
Short description:
Interested in formal verification of critical systems (targeting SIL-3 and -4) ? This topic looks at Railway infrastructure designs, together with the industry partner Anacon AS. The topic involves the use of the successful tool iSAT for verifying safety properties for a case study that Anacon works with.

The particular difficulty with safety-critical systems is that they are combining controller components, having discrete behaviour, with physical components, having continuous behaviour. This makes safety-critical systems part of what is more generally called cyber-physical systems since the controllers are usually computerized.

The student will learn to use the verification tool iSAT and how to model hybrid systems. The project may include software development to integrate the iSAT tools set into the framework of Anacon.

You may be spending time in the Anacon company, which designs railway infrastructures such as rail track designs or complete railway stations.

Alternative supervisors: Christian Johansen, Martin Steffen, Anacon AS
Read more details ...
As learning outcomes, the student will learn to work with the formal tool set iSAT and will learn how to model safety critical systems which are of a hybrid nature, i.e., involve both continuous and discrete behaviours. For modelling hybrid systems it is good if the student is inclined towards learning some needed mathematics, like differential algebraic equations and SAT solving.

The practical part of the topic can also be more towards implementation, and look at how the iSAT tools can be integrated in the software that Anacon uses. This involves looking at coupling/translations between the input languages of the different software. This could also involve working with finding good translation methods between the informal rules that govern railway designs, and the input language of the formal tool.

For mastering the iSAT tools there could be possibilities for visits abroad to eg. Germany in the group in Oldenburg actively developing iSAT. (Such visits, possibly to other places, are usually discussed during the master project, depending on the actual direction taken and on the motivation of the student.)

Automating railway designs

up to top
Short description:
For those interested in complex software systems with high safety requirements this topic looks at software used in the railway systems. In particular, this project is done in cooperation with Anacon AS, where the student may also take up a paid part-time job if selected by Anacon AS.

This topic looks at railway infrastructure designs and how to automate more the manual processes involved here. Of particular interest will be the interlocking or signalling system and how to integrate existing tools for these systems into the design work-flows. These are safety-critical components of the railway system, and much work has been done on formal verification of their required properties. But this work has not been included in the larger design and development cycle.

Alternative supervisors: Christian Johansen, Martin Steffen, Anacon AS
Read more details ...
When designing railway infrastructures like train stations or tracks there are involved complex tools like AutoCAD to get the physical and mathematical aspects in place, but also a lot of manual processes involving building large tables of values for the positioning of the various signals and other interlocking equipment. Maintaining these tables is hard when wanting to have a more agile style of design where changes are more often (maybe caused by discussions with authorities and decision makers, or from unexpected situations discovered in the field during the actual building of infrastructure, or from applying capacity optimization tools).

As learning outcomes, the student will learn to work with the formal tools used for analysing interlocking systems, like . Moreover, the student will gain knowledge about the software and terminology used in the railway systems sector. If the student has programming inclination then this project will offer the possibility to participate in a larger software project. Among the tools and technologies that a student may face can be: RailML markup language for describing railway designs, the OpenTrack software stack, iSAT model checker for safety properties verification, Prover from Sweden, SCADE from France Esterel technologies etc.

The practical part of the topic can also be more towards implementation, and look at how the formal tools can be integrated in the software that Anacon uses. This involves looking at coupling/translations between the input languages of the different software.

This topic is on purpose left open and general because there are many interesting small problems one can take. Which exact aspect to focus on will be discussed with the students.

Anacon AS has an ongoing internship announcement opened to outstanding students, which can be viewed here.

Engine for GML – Geography Markup Language

up to top
Short description:
If you programmed a web-interface incorporating maps, then you are probably familiar with Leaflet or OpenLayers, projects under the Open Source Geospatial Foundation. A main standard such tools support is the GML – Geography Markup Language developed by the Open Geospatial Consortium. While there are many things to explore here, one of immediate interest is IndoorGML for indoor positioning and rich semantical description.

This topic involves the development of an engine/tool for IndoorGML in Java. Features of this tool could include parsing and generating IndoorGML files. This tool would be coupled with the Tellu platform, thus integrated in this development environment, which already has some forms of indoor positioning. Thus, the student may be spending time in the Tellu company.

Alternative supervisors: Christian Johansen, Martin Steffen, Tellu AS
Read more details ...
As learning outcomes, the student will become familiar with standards for geolocation languages and tools like those around GML. In particular with the less spread aspect of Indoor location and the Indoor GML. At the same time, the student will gain knowledge of building tools for such XML-based languages and learn how to integrate such tools with more complex software systems, as those of Tellu.

The practical part of the topic is software development in Java, because the Tellu platform is developed in Java. But the programming language is not a restriction, and alternatives can be discussed. You may also need to learn to use other integration tools like Maven.

Interesting alternatives include the following.

  • For the student with knowledge of security and access control, the GeoXACML language profile of the popular standard XACML, which stands for “eXtensible Access Control Markup Language” and is developed as a standard by the OASIS standardization organization (with members of this committee being IBM, RedHat, Oracle, Microsoft, Cisco, Boeing and some 5 more). This combines geolocation and access control. This could be seen as also related to the topic XACML Drools.
  • For the student interested in semantics, ontologies, and semantics web, then GeoSPARQL would be interesting.

There is also the possibility to take an internship with Tellu.

Access Control Engines

up to top
Short description:
Interested in security and access control? Then you want to look at the XACML standard for describing access control policies.

One good start in this topic is through the Drools engine (which is part of a large family of RedHat JBoss components). Already an XACML engine exists as a JBoss component called PicketBox, but this handles only XACML 2.0. Can you extend it to the current 3.0 version?

You may be spending time in the Tellu company, which has Drools at the core of their products and are interested in access control.

Drools, as well as the jBPM6 component for Business Processes Management, could benefit greatly from a thorough study into access control policies and management. Of particular interest is how XACML fits with these rule-based engines.

Knowledge of Java is needed, because Drools, jBPM6, and PicketBox are build in Java (Drools uses Java Beans). Drools is a Rules Engine (among other things) developed by the RedHat community which is very much concerned with optimization of their projects and conforming with international standards.

But study into other access control engines is very encouraged.

Alternative supervisors: Christian Johansen, Audun Jøsang, Tellu AS
Read more details ...
As learning outcomes, the student will become familiar with RedHat’s JBoss Drools engine and probably with the XACML engine PicketBox. The student will become expert in the XACML 3.0 standard and will be familiar with other existing related standards, like the SAML 2.0, as well as with other existing engines like the Balana. Moreover, the student could gain experience with contributing to a large scale software project maintained by an open-source community.

XACML stands for “eXtensible Access Control Markup Language” and is developed as a standard by the OASIS standardization organization (with members of this committee being IBM, RedHat, Oracle, Microsoft, Cisco, Boeing and some 5 more).

The practical part of the topic is work with the Drools Java-based rule engine or to extend the PicketBox engine. This involves Java programming and rule-based programming (in the case of Drools). But this involves also work and understanding of a complex software application. In both cases the communities are helpful and the student will certainly find help there. Here is a good starting source for PicketBox, and here is a good source for starting with XACML authentication. The documentation for XACML 3.0 is easy to find.

The student can also take a case study coming from one of Tellu’s existing applications.

The topic is not restricted to Drools. The topic is focused on access control engines of any kind.

For rule engines and rule-based programming, Tellu AS can provide the necessary interaction; and the student may spend time (internship) in the company. For access control and related standards, the ConSeRNS group is a good place.

Business Process Engineering – the JBoss way

up to top
Short description:
Want to learn about the new paradigm of Business Process Modelling and how it applies to more than systems development? This project looks at the jBPM6 process engine from the RedHat JBoss family, and related components like the KIE Workbench and the Drools engine (which is the core Rules Engine). Knowledge of Java is needed, because jBPM6 is build on the Java Beans.

One practical goal can be to extend the jBPM6 with features from BPMN 2.0 which are not currently supported. A more ambitious goal is to make these extensions together with the jBPM6 developer community and in such a good way that it will be taken up i the next release.

You may be spending time in the Tellu company working on a case study from them.

Alternative supervisors: Christian Johansen, Tellu AS
Read more details ...
As learning outcomes, the student will know the industry standard BPMN 2.0 and will know how to specify processes with a graphical tool like the KIE Workbench of the JBoss family. The student will also know how the jBPM6 works and how it interacts with other essential components like the Drools rule engine. The JBoss tools suite is a leading on the market segment and is also open-source. This implies that often it is the solution of choice for many industry actors. The following book will be useful: “jBPM6 Developer Guide”.

The practical part of the topic is work with the jBPM6 Java-based process engine and programming environment. The student will also be exposed to more complex system development techniques by putting together several components of the JBoss family to work together, e.g., persistency, audit, or bus components. The student should not be afraid of Java programming, nor should be afraid of reading and using new tools like Maven or Apache Tomcat.

The student will take a case study coming from one of Tellu’s existing applications.

Logical Drools – advanced logical notions in the Drools engine

up to top
Short description:
Are you interested in logics in computer science, then you probably know of classical logic programming and rule-based reasoning (Horn clauses like if-then programming constructs). Rule based reasoning is used in many areas having to do with artificial intelligence (or where the problem to solve is not that simple) like for building Expert Systems. The Drools engine is one of the predominant choices in industry (and it is also open-source) developed by the RedHat community.

This topic is for someone that is ready for other non-standard logics, which are of high importance for Drools, like logics of Belief, Fuzzy logics, and logics of Knowledge used in the semantic Web. You would have to look into implementing into the existing Drools engine support for one of these kinds of reasoning.

You may be spending time in the Tellu company, which has Drools at the core of their products and are interested in applying it to ever more challenging problems.

Alternative supervisors: Christian Johansen, Martin Steffen, Tellu AS
Read more details ...
As learning outcomes, the student will become familiar with RedHat’s JBoss Drools engine and will know how to write rules in the DRL input language of Drools. Thus, by the end of the master studies, the student will have basic knowledge of rule-based programming. Besides this the student will gain knowledge of a different kind of logic, as mentioned before, and how such reasoning can be implemented. Moreover, the student will gain experience with contributing to a large scale software project maintained by an open-source community, which is Drools.

The practical part of the topic is work with the Drools Java-based rule engine and programming environment, and at the same time will involve working with existing implementations of the special kind of logic that will be chosen. In particular, we are interested in implementing (fully or partly) such new reasoning capabilities within Drools. To help with this a case study will be taken which would involve the new kind of reasoning. The case study can be taken from IoT, where Tellu AS has activities, or from the Railway domain where Anacon AS has activity.

Internships are expected within the company that we will work with (and paid part-time positions are possible for exceptional students).

Auto-scaling and Load-balancing in Amazon

up to top
Short description:
Interested in Cloud Systems ? Then working with auto-scaling and load balancing is the more challenging part. There are many aspects to deal with, and the concrete Cloud platform of Tellu is a perfect starting point. This is based on Amazon cloud (AWS), which is also one of the more advanced when it comes to auto-scaling capabilities.

Knowledge of Java is needed, because Tellu Cloud is programmed mainly in Java.

You will be spending time in the Tellu company, which is constantly improving their cloud platform.

Read more details ...
As learning outcomes, the student will become familiar with Amazon Cloud system (AWS) and the various functionalities they provide for auto-scaling, like auto-scaling groups, load-balancers, metrics, alarms, topics, queues, or cloud watch. Thus, by the end of the master studies, the student will have strong knowledge of cloud systems in general and the AWS in particular. The student will learn other related technologies which are essential when building cloud systems, like CoreOS, Docker, Fleet, Mediator and SOA patterns, etc.

The practical part of the topic is to work with the Tellu Cloud platform and test various auto-scaling scenarios. This involves both AWS setup work and testing, as well as implementation. Depending on the tasks taken, these practical aspects can be more or less demanding and technical.

The theoretical part of the topic is to model and analyse the gains given by the auto-scaling approach. This has the goal to provide more concrete and verifiable guarantees about the system being auto-scaled (like, no message will be kept waiting more than 30s; or downtime is in-existent).

The topic can go in either ways (or in both). The student will take a case study coming from one of Tellu’s existing applications.

Tellu can provide the necessary infrastructure and interaction; and the student may spend time (maybe internship or part-time) in the company.

4  Energy Informatics

Some related links are: energyinformatics.info, the USC Center For Energy Informatics.

Related books include: eBook “Energy Informatics” by Richard Watson and Marie-Claude Boudreau;

4.1  Optimization Problems

CityBikes – learning and optimizing the service

up to top
Short description:
This project involves the conceptualization and development of a planning system (based on extensions of the traveling salesman algorithm) to be used by service maintainers of the Oslo CityBikes system. The system could also involve learning typical behavior of each bike rack and predictions. The planning system would have both a front-end (as for a mobile device like GPS or Palm/mobile) and a back-end where the information processing and decision taking is done for each user separately and coordinated.
Alternative supervisors: Olaf Owe, Christian Johansen
Read more details ...

Electric cars guidance

up to top
Short description:
This project studies and continues the recent work of Martin Leucker (and others like GreenNavigation project). It is supposed to develop algorithms and tools/applications to be used in the electric cars. Starting point are navigation systems. Other investigations can be done on ways to improve battery life cycle.

4.2  Smart Electric Grid

Smart Electric Grid

up to top
Short description:
This is a general topic that can span many master projects. The general idea is to investigate how to use computer science techniques and algorithms to achieve the vision of EU for a efficient, sustainable, reliable, and flexible distribution of energy at the European level (and ultimately world level). The master subjects can vary from investigation of existing projects and literature with a comparative and critical purpose, to load balancing algorithms on dynamic network structures. Most of the technical developments would involve modeling of the proposed solutions; i.e., modeling of smart electric grids, and evaluation/investigation of various proposed solutions/properties/problems.

See related links as: European Electricity Grid Initiative or Smart grid news.

Alternative supervisors: Christian Johansen, Olaf Owe, Frank Eliassen
Read more details ...
There is much recent work on the many facets of the Smart Electric Grid, showing the immediacy of this problem and the high environmental and economic interest of EU. Speaking purely theoretical, there are many advanced techniques for solving the issues related to computer science, like load balancing, distributed algorithms, or dynamic network topologies. But the more general obstacles come from the social perspective, like privacy issues, or security of a computer controlled global energy infrastructure, availability, or fairness in using such a global framework by those in decision power.

The master subjects can investigate how information technology can be used to leverage also these social concerns. For example, one may model a proposed framework and test availability properties (liveness properties), or may study implementation of fairness mechanisms directly in the framework, automatic, without human intervention. Moreover, many kinds of privacy issues can also be solved automatically and implemented in the global smart grid framework.

More technical/algorithmic investigations also can find place, as there is good room for improvement of existing techniques.

5  Ubiquitous Systems (Internet of Things)

This is a recent trend in the European Union that involves all aspects of computing and engineering. This topic is more oriented towards applications, but there is also a good deal of theoretical challenges for those that want that. Applications of ubiquitous computing (also more trendy called IoT) is envisioned for various things such as: interactive hospital, ambient assisted living, green intelligent buildings, ubiquitous city (as lead by S.Korea), distributed and embedded systems as in cars or airplanes, etc.

See a long list of resources at the IFI Library

This general area is open for discussions. There are many topics that could fit in some of our current projects, like IoTSec or Models4IoT. Below are a small selection; come by our offices if you want to discuss alternatives that could fit you.

Programming IoT with UML

up to top
Short description:
IoT involves many kinds of small devices with limited capabilities. In consequence different programming concerns are raised, as opposed to classic object-oriented programming. Many of the languages are more low-level, like C or nesC (of Contiki or TinyOS) and less easy to master. In this project you will use a different approach, based on modelling and automatic code generation. The tool that will be used is the QP-nano. This is specially designed for resource constrained systems. The tool is part of a tool suite coming from QuantumLeaps and has also a book written about it, which the student will study.
Alternative supervisors: Christian Johansen, Olaf Owe, Frank Eliassen
Read more details ...
As learning outcomes, the student will gain knowledge with the QP tool framework, in particular with the QP-nano for wireless sensors and embedded systems. One would learn how to develop IoT systems by modeling and generating the implementation code. The modeling is done using a graphical language. This is highly attractive for industry people, both because of the visual language and because of the code generation. Even more, the model can be used for verification purposes, which is highly desired for safety-critical systems, e.g., as those that DNV or Thales is working with.

Internship and collaboration opportunities exist with companies like Tellu (Asker).

Programming IoT with ThingML

up to top
Short description:
This topic involves developing IoT systems with a graphical language and development environment called ThingML and developed partly by SINTEF in collaboration with international partners in European projects. IoT involves many kinds of small devices with limited capabilities. In consequence different programming concerns are raised, as opposed to classic object-oriented programming. Many of the languages are more low-level, like C or nesC (of Contiki or TinyOS) and less easy to master. In this project you will use a different approach, based on graphical languages and automatic code generation.
Alternative supervisors: Christian Johansen, Olaf Owe
Read more details ...
As learning outcomes, the student will gain knowledge with the ThingML framework, and probably with related environments like Kevoree. One would learn how to develop IoT systems by modeling and generating the implementation code. The modeling is done using a graphical language. This is highly attractive for industry people, both because of the visual language and because of the code generation.

Internship and collaboration opportunities exist with companies like Tellu (Asker) and SINTEF as well as possible travel to international partners in the HEADS project.

6  Practical Applications of Theory

6.1  Security and electronic voting

Analysing PGP Pretty Good Privacy

up to top
Short description:
This project involves looking into PGP encryption and the protocols and security technology around it. PGP can be used in many places, like e-mail security and privacy, or to strongly encrypt information. There are various implementations of the standard OpenPGP like the GNU Privacy Guard and plugins for e-mail clients like Enigmail for Thunderbird. Interesting with PGP is also the trust model that it is proposed, because it contrasts with the standard PKI, which is always contested.

Depending on the motivation and abilities of the student, this project could collaborate with NTNU researcher on security from the group of Colin Boyd.

Alternative supervisors: Christian Johansen, Audun Jøsang
Read more details ...
Various paths can be explored and we decide that together with the student.

One possibility is to use existing tools for analysing security protocols, like ProVerif or Murphi. One would look into how to model parts of PGP, and then use the tools to verify security properties of them individually or when put together, which is more challenging.

One can also choose to do a more empirical and practical analysis of the PGP adoption, or usability.

One can look into the various open source implementations of PGP. You will need to look closer in the documentation, like the documentations or books also one written by Zimmerman.

Analysing Bitcoin-like Crypto-currencies

up to top
Short description:
This project involves looking into Bitcoin and the protocols and security technology behind it. You should expect to work with newly introduced technologies like Bitcoin consensus and distributed peer-to-peer network algorithms, or Block-chain style of distributed write-only database, or proof-of-work algorithms.

Depending on the motivation and abilities of the student, this project include work on developing a new Crypto-currency for Science, which is a project initiated by Stefan Krauss.

Alternative supervisors: Christian Johansen, Audun Jøsang, Stefan Krauss
Read more details ...
Various paths can be explored and we decide that together with the student.

One possibility is to use existing tools for analysing security protocols, like ProVerif or Murphi. One would look into how to model one or several of the protocols involved in Bitcoin, and then use the tools to verify security properties of them individually and when put together, which is more challenging. Some preliminary work is using Uppaal.

One can also choose to do a more empirical and practical analysis of the Bitcoin network, but this has been done by more people (e.g.: by Clemens H. Cap, or The Bitcoin Backbone Protocol: Analysis and Applications, or Quantitative Analysis of the Full Bitcoin Transaction Graph), than the above approach based on formal tools. Still many aspects can be explored here as well.

Another possibility is to look into privacy and anonymity aspects of Bitcoin and other similar currencies like the Zerocoin paper (which is a bit mathematical, but other resources exist on their website).

Yet another possibility is to look into the whole implementation system, the bitcoind project, which many say it is a wonderful piece of software programming (e.g. see Dan Kaminsky opinion). Here are many on-line resources, e.g.: Bitcoin Developer Reference,

There exist a few works on Bitcoin, and the student can start from them (e.g.: A good MSc thesis, A good Book “Mastering Bitcoin” by Andreas M. Antonopoulos, A nice Overview of Challenges for Bitcoin, good resources from a Crypto-Course). The technologies that Bitcoin popularized are quite impressive, e.g. see the adoption of the block-chain idea by the Linux Foundation in their Hyperledger project.

Privacy certification of mobile Apps

up to top
Short description:
You know how to program Apps (like for Android) and you know what kind of privacy information can be derived from the location information revealed by a mobile phone. You are interested in gaining deep knowledge of App programming, of location information analysis, and of privacy related aspects (even legal).

In this topic you will work to prove practically what kind of privacy can be revealed, how such revealing can be hidden from the user, how it can be hidden even from experts that want to analyse the app, and how all these can be solved through a process of certification. You will in fact need to work out a certification process, and see if this process can indeed distinguish privacy preserving apps from privacy infringing apps.

Alternative supervisors: Christian Johansen, Josef Noll
Read more details ...
Various paths can be explored and we decide that together with the student.

Should we test real existing apps? (Which ones?)

Implementing Actor Network Theory for Security

up to top
Short description:
Sociology devised the Actor Network Theory which inspired recently work on graphical formalisms for security ceremonies. You would look into how to implement a tool to work with such a graphical formalism for modeling security ceremonies.
Alternative supervisors: Christian Johansen, Olaf Owe, Audun Jøsang

Privacy and security in the Norwegian eVoting system

up to top
Short description:
This project involves looking into eVoting protocols with a special interest into the newly introduced Norwegian eVoting system.

Depending on the motivation and abilities of the student, this project can include a one semester exchange with IT University of Copenhagen. This project could also involve interaction with the Norwegian ministry of local government and modernization, which is taking care of implementing eVoting in Norway.

Alternative supervisors: Christian Johansen, Olaf Owe, Audun Jøsang
Read more details ...
Various paths can be explored and we decide that together with the student.

One possibility is to use existing tools for analyzing security protocols, like ProVerif or Murphi. One would look into how to model the eVoting protocol, and in fact the whole implementation system, and then use the tools to verify security properties of the protocol and the whole system.

Another possibility is to look into privacy aspects of the eVoting protocols.

Yet another possibility is to look into proof techniques for security protocols. Then apply such a technique to prove (i.e., have mathematical guarantees for) security properties of the eVoting protocol.

Yet another possibility is to look into algebraic homomorphic encryption. This is a hot topic in cryptography with good application to complicated eVoting schemes (like the one we have in Norway). This topic would be for a highly motivated student.

Cognitive Causes of Security Breaches

up to top
Short description:
This project involves a cases study and analysis of human users of a security ceremony; i.e., security protocol or procedure where the human is part of the protocol. The current on-line banking is an example, or the recent electronic voting procedure used in Norway. This topic is at the border of security and psychology. Your work will start from a recent paper [34] originating from the group of Ann Blandford.
Alternative supervisors: Christian Johansen, Audun Jøsang, Olaf Owe

Typing and Subtyping for Security

up to top
Short description:
This project involves working with typing systems (one needs background from a course like ) to guarantee security properties. A cases study of a security protocol will guide the work. Your work will start from investigating existing research papers on this topic, like [20, 15, 16, 2, 1], as well as studying the specification of a security protocol/ceremony, like ZRTP or OTR.

Analyzing Off-The-Record messaging

up to top
Short description:
This project involves working with the protocol suite called Off-the-record OTR. The student will first learn about the specification of this protocol and about tools and techniques for analyzing security/communication protocols like Murphi from the Stanford security lab, the AVISPA, or the FDR3 from Oxford. The goal is to model the OTR protocol [8] and analyze security/privacy properties of it. A starting point will be the papers [33, 35].
Alternative supervisors: Christian Johansen, Olaf Owe, Audun Jøsang

Off-the-record Implementations

up to top
Short description:
This project involves working with (looking in the code of) implementations of OTR communication protocol. In particular you would look at the Jitsi messaging client and its open source code implementation in Java. Communication with the current Jitsi developers is expected. This topic can get different focus directions. One could be to work with verification tools for Java code, and to verify security properties of the OTR protocol on its implementation in Jitsi. Another direction can be to concentrate only on the OTR implementation and see that it conforms with the official specification.
Alternative supervisors: Christian Johansen, Olaf Owe, Audun Jøsang
Read more details ...
This project can also include, to some extent, use of automated tools for Java code, like the model checking tool Bandera from SantosLab or the Java Pathfinder. An alternative path in this project could be to look at the implementations of the encryption protocols used in Jutsi, like the ZRTP.

Analyzing VoIP protocols

up to top
Short description:
Voice over IP (VoIP) is a technology for audio communications over IP which is wide spread. This project is concerned with protocols that this technology is based on, especially the Session Initiation Protocol (SIP) and the ZRTP encryption protocol. One would read and understand the specifications for these protocols (we choose one) and then work with formalisms and tools to model and analyze the respective protocol.
Alternative supervisors: Christian Johansen, Olaf Owe, Audun Jøsang
Read more details ...
Various paths can be explored and we decide that together with the student.

One possibility is to start from the paper [9] and the master project from Stanford that uses the Murphi tool.

Another possibility is to look at implementations of one such protocol into an existing SIP - VoIP client like the GPL Jitsi.

SHA-3 implementation and analysis

up to top
Short description:
SHA-3 is the latest cryptographic hash function algorithm suite adopted by the NIST in USA. The precursor SHA-1 which is widely used should become obsolete (Microsoft and Goolge will stop using them in 2017) and are being replaced by the second generation of such algorithms called generically SHA-2. Several implementations exist, usually done by the main players in the arena, like the RSA.

This master topic will look at the latest generation, SHA-3, for which there are not many implementations out there. Moreover, the implementation that you will make will have to be accompanied by a verification part which would prove that the implemented code indeed does what the NIST specification says. Which implementation framework and language to use is open and will be decided together; and the same for the verification approach and tools.

Alternative supervisors: Christian Johansen, Olaf Owe, Audun Jøsang
Read more details ...

6.2  Legal Electronic Contracts

Formalizing iTunes

up to top
Short description:
This project involves working with natural language processing technologies, in particular the controlled natural languages such as the Attepto Controlled English (ACE). The project takes the Terms of Services (ToS) of iTunes (a legal contract) as a case study and works on the way to automatically read it using the available tools for such a natural language processing task. At the end this project will offer a technology for translating any Internet ToS into a computer model which can be further analyzed by others through logical techniques.

Depending on the motivation and abilities of the student, this project can include a one semester exchange with Zurich University or Gothenburg/Chalmers University.

Alternative supervisors: Christian Johansen, Olaf Owe

Tools for Electronic Contracts – a survey

up to top
Short description:
This project is particularly suited for a student who enjoys reading and studying literature in a comparative and meticulous style, but does not necessarily enjoy crunching down on a single particular problem. This project will not involve programming/implementation, but it could involve experimenting with various existing tools, possibly comparing them with respect to certain predefined criteria.

The social motivation of this project comes from the need to have legal contracts (like the Terms of Services on the Internet) put through such a tool so to ease their drafting and analysis.

Alternative supervisors: Christian Johansen, Olaf Owe

Check Properties of Legal Electronic Contracts

up to top
Short description:
This projects involves the implementation of a model checking tool for legal electronic contracts expressed in some contract logic. Alternatively, you may use an existing model checking tool and logic to model legal contracts and to check properties on them.
Alternative supervisors: Martin Steffen, Christian Johansen, Gerardo Schneider

Reading legal contracts

up to top
Short description:
This project involves natural language processing. The ultimate goal is to translate a legal contract written in plain natural language into a contracts logic. This is rather difficult and therefore one may start with translating legal contracts written in a restricted form of natural language. This project involves the use of the latest theories in natural language processing, and implementing these for a specific form of constraint language dedicated for legal contracts.
Alternative supervisors: Olaf Owe, Christian Johansen, Stephan Oepen

6.3  Universal Algebra

Using Automated Theorem Provers in the Context of Synchronous Kleene Algebra

up to top
Short description:
This projects involve the use of theorem provers like the general Isabelle or Coq, or specialized provers for equational systems like Prover9. One would have to start from existing work on Kleene algebra and related theorem provers, and work its way to the new formalism of Synchronous Kleene Algebra (or the related Concurrent Kleene Algebra). This project can involve either just using existing tools and checking various useful theorems, or may involve building extensions and libraries specific for these two concurrent variants of Kleene algebra.
Alternative supervisors: Volker Stolz, Christian Johansen
Read more details ...
Kleene Algebra (see a nice tutorial/course of Dexter Kozen) is an old formalism (initiated by Stephen Kleene and developed by John Conway) which you use, without even knowing maybe, in many places in your daily programmers work, like in regular expressions, essential programming language constructs, automata theory, logics, etc. Reasoning in Kleene algebra uses equational reasoning, so provers are fairly happy with it.

There are many extensions (and uses) of Kleene algebra, and the to that you could concentrate on in this master topic are the recent concurrent extensions: Synchronous Kleene Algebra [31] and Concurrent Kleene Algebra [18]. Several other new interesting extensions of Kleene algebra, useful in programming, can be tackled also, like [11, 19, 29].

One of the people working on Kleene algebras and extensions, also using provers, is Georg Struth, in Leicester, UK. We will be following/extending/using some of his work, like that using Isabelle here, or that using Prover9 here.

Modeling with (Synchronous) Kleene Algebra

up to top
Short description:
This topic would involve modeling examples of systems using Kleene algebra (for sequential/regular systems) and Synchronous/Concurrent Kleene algebra (for systems involving notions of concurrency). This topic may also involve working with other associated formalisms for modeling systems; formalisms which have close connections with Kleene algebra, like translations and correlations. For the more new concurrent/synchronous variants of Kleene algebra one may build formalisms/languages/tools on top of the algebraic language, and use those for modeling.
Alternative supervisors: Olaf Owe, Christian Johansen

Programming in (Synchronous) Kleene Algebra

up to top
Short description:
This topic involves working with programming languages constructs, at a basic level. It is known that Kleene algebra with tests (see the work of Dexter Kozen and the KAT prover) is at the basis of essential programming constructs. This topic would investigate what kind of system/programs can be written using the synchronous and concurrent variants of Kleene algebra. This topic would involve working with examples.
Alternative supervisors: Olaf Owe, Martin Steffen, Christian Johansen
Read more details ...
Related research articles include [26, 3, 25, 22, 10, 23, 24, 27, 4, 21].

Verifying Properties of Systems using Kleene Algebra

up to top

6.4  Concurrency and Parallelism

Modeling with Events

up to top
Short description:
This project involves the more practical matters about using event-based concurrency models for describing concurrent/parallel systems. Case studies will be taken. Investigations into the various event-based models will be made, including evaluating these with respect to the taken case studies.

Programming with True Concurrency

up to top
Short description:
This project will look into the possibilities of programming concurrent software using the event-based concurrency paradigm. The project will investigate programming constructs in the various event-based models. Simple programming examples are to be investigated. The project could also involve the development of related programming tools.
Alternative supervisors: Olaf Owe, Christian Johansen

Tools for visualizing and working with Higher Dimensional Automata

up to top
Short description:
This topic involves understanding the formalism of Higher Dimensional Automata (HDA) and then developing visualization techniques for these. Alongside a software tool for visualizing HDA will be developed. HDA are the most expressive model of concurrency. HDA are normally thought in higher geometrical spaces (this means not just 3D). One can also investigate a visual development tool, which will not just visualize the HDA but also allow the user to define/construct HDA models in the graphical manner.

Tools for visualizing and programming with Transactions

up to top
Short description:
This topic involves developing a method and associated tools for visualizing transactions, as in transactional concurrent programming paradigm. First an investigation into the existing tools and methods is to be done. Case studies can be carried out.
Alternative supervisors: Martin Steffen, Christian Johansen

Working with Chu

up to top
Short description:
Modeling concurrent systems with Chu spaces and using the tool Chu Calculator. This topic is for a more mathematically inclined person, but the project is about applying and using the mathematical framework/theory of Chu spaces.

Working with Live Sequence Charts

up to top
Short description:
This project involves understanding Live Sequence Charts (see the book Come, Let’s Play of David Harel and Rami Marelly; available also for download) and the associated tool set Play-Engine. One can check a similar master outcome at the IFI Library. Live Sequence Charts are a formalism for modeling concurrent/parallel systems; and may be familiar to the Message Sequence Charts of UML and to the older formalism for concurrent and reactive systems Statecharts (see the book and the commercial tool Statemate).
Alternative supervisors: Volker Stolz, Christian Johansen

Reason about programs with DL and work with the Key tool

up to top
Short description:
This project involves understanding Dynamic Logic (see the book of David Harel, Dexter Kozen and Jerzy Tiuryn; available also at the IFI library). This powerful method of checking functional/logical properties of programs was implemented in the tool Key. The master project would involve surveying literature and working on concrete case studies.
Read more details ...
Much of the work of Dexter Kozen on Kleene algebras is related to Dynamic Logic and reasoning about programs. So there is also room for more theoretical investigations. But otherwise this project is about understanding what it means to reason about programs and how to work with a tool like Key. A Key Book accompanies the tool and explains the theory behind it. There are also various user manuals and examples on the KeY website (eg. a gentle introduction paper).
Alternative supervisors: Olaf Owe, Crystal Din, Christian Johansen

SOS for Distributed OO Programming and the Rewriting Logic

up to top
Short description:
This project involves understanding Rewriting Logic and the Maude tool. The master project would involve surveying literature and working on concrete semantics of programming languages. One would work on redefining semantics written in the Rewriting Logic style into the SOS style. Various related issues can be investigated along the way.
Read more details ...
A gentle introductory book on SOS can be found at the IFI library.
Alternative supervisors: Olaf Owe, Christian Johansen

6.5  Process Calculi

Programming/modeling of mobile systems with Bigraphs

up to top
Short description:
Use (or extend) the existing tool set for Bigraphs of Thomas Hildebrandt and team, which is an outcome of the project Bigraphical Programming Languages (BPL).
Read more details ...
For a list of documentation on the bigraphs formalism check the online Bibliography on Bigraphs.

Applications or Implementations of Decomposition methods based on Rule Formats

up to top
Short description:
One would have to investigate applications to case studies of the decomposition methods based on rule formats. Case studies include definitions of semantics of programming languages or of process algebras based on structural operational semantics. There is an initial required reading of the relevant papers on this topic. One can also choose to work on implementations of these methods and connect it to some existing model checker tool.
Read more details ...
For a list of essential readings for this master topic check [14, 30, 17, 7, 13]. For the implementation issues one would also read some related works on optimizations for such techniques, eg. [5, 28].

6.6  Verification of Properties for Programs or Systems

Model Checking Creol/ABS Programs with Spin

up to top
Short description:
This topic involves understanding the programming language of Creol (or the more modeling oriented ABS) which is developed in the PMA group. This is an object-oriented, distributed programming language. After getting a grip on programming in Creol one would look into how to model check programs written in Creol using the model checking tool called Spin. Therefore, one would also gain knowledge of model checking of programs (Spin is essentially working with C-like programs) and of working with the Spin tool. The model checking course INF5140 teaches model checking.
Read more details ...
Essentially the topic would involve practical work with the specification language of the Spin tool and the programming language Creol. The outcome is a translation/encoding of Creol programs in Spin, so to be ready for model checking.

Formal Semantics for JavaScript

up to top
Short description:
This topic is concerned with formal/mathematical semantics for the well known JavaScript interpreted language (see the standard 258p description file). The work starts with studying the 2008 APLAS paper, and related subsequent results, directed to giving formal semantics to JavaScript. Part of the reading will also involve getting acquainted with the classic works on structural operational semantics for programming languages in general (see a book in the IFI library).

The practical benefits of having a formal semantics for a language like JavaScript are multiple: from clear implementation guidelines (so that browsers will no longer implement their own understanding of how JavaScript should work, but use the clear formal description), to verification and testing tools (like the ones done by eg. Anders Moller in the TAJS project), to opening the possibility to a multitude of related formal/mathematical results for JavaScript (like optimization issues, or other kinds of semantics like axiomatic or denotational, or comparisons/integrations of features with other languages like HTML5).

Alternative supervisors: Olaf Owe, Christian Johansen, Volker Stolz, Crystal Din

7  Theoretical Topics

7.1  Legal Electronic Contracts

The Constrained Natural Language of the Legal Electronic Contracts

up to top
Short description:
In this project one must develop a restricted form of natural language to be used for writing legal contracts. This is supposed to be used by both machine and human. This will make it possible that the computer reads a legal contract and interprets it in some form of contracts logic. This is a first step to automate the processing of legal contracts. In this way the computer can read and communicate human-understandable legal contracts. It cannot understand these contracts though. For this a contracts logic is needed (see topic Extend and improve the existing logics of contracts).
Alternative supervisors: Olaf Owe, Christian Johansen, Stephan Oepen

Extend and improve the existing logics of contracts

up to top
Short description:
This topic involves work within logics of contracts. Still the logics for contracts are in incipient forms. One needs to extend the existing ones. There are various directions here...
Alternative supervisors: Olaf Owe, Christian Johansen, Gerardo Schneider

7.2  Concurrency and Parallelism

Modeling with Events

up to top
Short description:
This topic involves the more theoretical aspects of event-based models of concurrency. This topic can involve comparative studies of the various concurrency models. Or it can involve extensions with time or probabilities. This topic can also involve more complex case studies of systems to be modeled with event-based concurrency formalisms, and an analysis of the drawbacks and possible solutions.

Programming with True Concurrency

up to top
Short description:
This topic involves more theoretical aspects of programming concurrent systems using notions and formalism coming from the event-based paradigm of concurrency. It can involve investigations into message-passing for such formalisms, or programming constructs coming from notions from event-based models.
Alternative supervisors: Olaf Owe, Christian Johansen

Verifying Properties of True Concurrent Systems

up to top
Short description:
This project involves investigations into the verification aspects of true concurrency models. This topic can involve studying logics for one of the event-based formalisms. It can involve study of the decision problems related to verification of properties for systems specified using event-based or partial orders-based models of concurrency. This topic is more challenging than standard verification of sequential systems, also because there are negative results about undecidability of some problems for some of the partial order-based models.

Highly Expressive True Concurrency Models

up to top
Short description:
This topic involves investigation into the expressive power of existing true concurrency models. It would involve understanding of the highly expressive models like Higher Dimensional Automata, or event structures, or configuration structures. It would involve comparative investigations into other existing related formalisms. This topic can also involve extensions of existing formalisms to capture additional aspects of concurrent systems, like agency, time, uncertainty, or communication.

Transforming Graphs

up to top
Short description:
This topic involves investigation of the literature on Graph Transformations and Graph grammars. One would then delve into either the many application areas or into the theoretical/mathematical problems in this topic.

Equivalences for True Concurrent Systems

up to top
Short description:
This topic involves investigation of the literature on equivalence notions and true concurrency systems. After a preliminary understanding of the basic notions involved, more interesting theoretical contributions will be investigated. There is also place for implementations, but this topic is mostly theoretical. More details are given on request.

7.3  Process Calculi

Extending Rule Formats

up to top
Short description:
This topic would investigate Rule Formats. These are useful in giving structural operational semantics, which, in turn, are used in many aspects, like in semantics of programming languages, or semantics of modeling and specification languages for various kinds of systems.

Compositional Reasoning using Rule Formats and their Logics

up to top
Short description:
This topic involves work with rule formats and modal logics to achieve compositional reasoning about systems. The project will involve investigation of the existing work on this issue. Possible extensions of these works will then constitute the novelty of the master project.

7.4  Algebra

Algebraic Theory of Object Oriented Programming

up to top
Short description:
This topic involves the investigation of algebraic theories of programming, and then reach the recent few works on algebraic approaches to object-oriented concepts of programming. Depending on the maturity of the student, this topic would end with touching on one of the many open research questions. We may also work with concurrent OO languages.
Alternative supervisors: Martin Steffen, Olaf Owe, Christian Johansen

7.5  Logic in Computer Science

Working with logics for Bigraphs

up to top
Short description:
This topic would investigate the few existing logics for the Bigraphs. The topic could also involve the design of new logics. The existing work is focused on spatial logics.

Working with logics for Higher Dimensional Automata

up to top
Short description:
This topic studies the few existing logics for the model of true concurrency called Higher Dimensional Automata. The topic can also consider logics for other models of concurrency. There are many open problems in this area, hence, many opportunities.

Working with logics of knowledge, belief, and communications

up to top
Short description:
This topic the interesting area of logics for modeling the knowledge of agents or their beliefs, and how the act of communicating some new information changes their knowledge or beliefs. There are many open research problems as well as practical applications scenarios to be investigated. Since the community of smart agents is growing very big, with many real-life case studies, there is need for tools like model checkers. Here is where implementation skills are needed.
Read more details ...
For your entertainment, and to get an idea of the interesting puzzles that are encountered with these logics of knowledge, belief, announcements, etc... check “The Russian cards problem” or “One hundred prisoners and a lightbulb”. The IFI Library has quite a number of references, eg. books: “Dynamic Epistemic Logic” or “Epistemic logic for AI and computer science”.

7.6  Machine Learning

Though I do not actively research in this field, I would be happy to supervise on any of the following emerging topics. These are of research character but with huge applications outcome. Moreover, many of these are inspired by biology, and hence rather powerful techniques.

Computational evolutionary embryogeny

up to top
Short description:
This topic would investigate the recent machine learning formalism called Computational evolutionary embryogeny. This formalism combines the more established field of Evolutionary computation with the more new field called Artificial Embryogeny.
Alternative supervisors: Olaf Owe, Christian Johansen

References

[1]
Martín Abadi (1999): Secrecy by Typing inSecurity Protocols. Journal of the ACM (JACM) 46(5), pp. 749–786, doi:http://dx.doi.org/10.1145/324133.324266. Available at https://dl.acm.org/citation.cfm?doid=324133.324266.
[2]
Martín Abadi & Bruno Blanchet (2003): Secrecy types for asymmetric communication. Theor. Comput. Sci. 3(298), pp. 387–415. Available at http://dx.doi.org/10.1016/S0304-3975(02)00863-0.
[3]
Kamal Aboul-Hosn & Dexter Kozen (2006): KAT-ML: an Interactive Theorem Prover for Kleene Algebra with Tests. Journal of Applied Non-Classical Logics 16(1-2), pp. 9–34.
[4]
Kamal Aboul-Hosn & Dexter Kozen (2008): Local Variable Scoping and Kleene Algebra with Tests. J. Log. Algebr. Program. 76(1), pp. 3–17.
[5]
Henrik Reif Andersen (1995): Partial Model Checking (Extended Abstract). In: 10th IEEE Symposium on Logic in Computer Science (LICS’95), IEEE Computer Society, pp. 398–407.
[6]
Giampaolo Bella & Lizzie Coles-Kemp (2012): Layered Analysis of Security Ceremonies. In Dimitris Gritzalis, Steven Furnell & Marianthi Theoharidou, editors: Information Security and Privacy Research - 27th IFIP TC 11 Information Security and Privacy Conference, SEC 2012, Heraklion, Crete, Greece, June 4-6, 2012. Proceedings, IFIP Advances in Information and Communication Technology 376, Springer, pp. 273–286. Available at http://dx.doi.org/10.1007/978-3-642-30436-1_23.
[7]
Bard Bloom, Wan Fokkink & Rob J. van Glabbeek (2004): Precongruence formats for decorated trace semantics. ACM Trans. Comput. Log. 5(1), pp. 26–78. Available at http://doi.acm.org/10.1145/963927.963929.
[8]
Nikita Borisov, Ian Goldberg & Eric A. Brewer (2004): Off-the-record communication, or, why not to use PGP. In Vijay Atluri, Paul F. Syverson & Sabrina De Capitani di Vimercati, editors: Proceedings of the 2004 ACM Workshop on Privacy in the Electronic Society, WPES 2004, ACM, pp. 77–84. Available at http://doi.acm.org/10.1145/1029179.1029200.
[9]
Riccardo Bresciani & Andrew Butterfield (2009): A formal security proof for the ZRTP Protocol. In: Proceedings of the 4th International Conference for Internet Technology and Secured Transactions (ICITST’09), IEEE, pp. 1–6. Available at http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5402595.
[10]
Ernie Cohen, Dexter Kozen, Frederick Smith, Ernie Cohen, Dexter Kozen & Frederick Smith (1996): Complexity of Kleene Algebra with Tests, The. Technical Report, Ithaca, NY, USA.
[11]
Jules Desharnais, Bernhard Möller & Georg Struth (2006): Kleene Algebra with Domain. ACM Trans. Comput. Log. 7(4), pp. 798–833. (available at ).
[12]
Carl Ellison (2007): Ceremony Design and Analysis. Cryptology ePrint Archive, Report 2007/399. Available at http://eprint.iacr.org/2007/399.
[13]
Wan Fokkink & Rob J. van Glabbeek (1996): Ntyft/Ntyxt Rules Reduce to Ntree Rules. Inf. Comput. 126(1), pp. 1–10. Available at http://dx.doi.org/10.1006/inco.1996.0030.
[14]
Wan Fokkink, Rob J. van Glabbeek & Paulien de Wind (2006): Compositionality of Hennessy-Milner logic by structural operational semantics. Theoretical Computer Science 354(3), pp. 421–440. Available at http://dx.doi.org/10.1016/j.tcs.2005.11.035.
[15]
Cédric Fournet, Andrew D. Gordon & Sergio Maffeis (2007): A type discipline for authorization policies. ACM Trans. Program. Lang. Syst. 29(5). Available at http://doi.acm.org/10.1145/1275497.1275500.
[16]
Andrew D. Gordon & Alan Jeffrey (2003): Authenticity by Typing for Security Protocols. Journal of Computer Security 11(4), pp. 451–520. Available at http://iospress.metapress.com/content/bhqqufra1c7w8tly/.
[17]
Jan Friso Groote & Frits W. Vaandrager (1992): Structured Operational Semantics and Bisimulation as a Congruence. Information and Computation 100(2), pp. 202–260. Available at http://dx.doi.org/10.1016/0890-5401(92)90013-6.
[18]
Tony Hoare, Bernhard Möller, Georg Struth & Ian Wehrman (2009): Concurrent Kleene Algebra. In Mario Bravetti & Gianluigi Zavattaro, editors: 20th International Conference on Concurrency Theory (CONCUR’09), Lecture Notes in Computer Science 5710, Springer, pp. 399–414. (available at ).
[19]
Peter Höfner & Georg Struth (2007): Automated Reasoning in Kleene Algebra. In Frank Pfenning, editor: 21st International Conference on Automated Deduction (CADE’07), Lecture Notes in Computer Science 4603, Springer, pp. 279–294. (available at ).
[20]
Hans Hüttel (2011): Typed psi-calculi. In Joost-Pieter Katoen & Barbara König, editors: CONCUR, Lecture Notes in Computer Science 6901, Springer, pp. 265–279. Available at http://dx.doi.org/10.1007/978-3-642-23217-6_18.
[21]
Dexter Kozen (1997): Kleene Algebra with Tests. ACM Transactions on Programming Languages and Systems (TOPLAS’97) 19(3), pp. 427–443.
[22]
Dexter Kozen (2003): Kleene Algebra with Tests and the Static Analysis of Programs. Technical Report.
[23]
Dexter Kozen (2008): Nonlocal Flow of Control and Kleene Algebra with Tests. In: 23rd IEEE Symposium on Logic in Computer Science (LICS’08), IEEE Computer Society, pp. 105–117.
[24]
Dexter Kozen & Dexter Kozen (1996): Kleene Algebra with Tests and Commutativity Conditions. In Tiziana Margaria, Bernhard Steffen, Tiziana Margaria & Bernhard Steffen, editors: 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS’96), Lecture Notes in Computer Science 1055, Springer, pp. 14–33.
[25]
Dexter Kozen & Dexter Kozen (1998): Typed Kleene Algebra. Technical Report 1669.
[26]
Dexter Kozen & Dexter Kozen (2000): On Hoare Logic and Kleene Algebra with Tests. Transactions on Computational Logic 1(1), pp. 60–76.
[27]
Dexter Kozen & Maria-Christina Patron (2000): Certification of Compiler Optimizations Using Kleene Algebra with Tests. In: Computational Logic, pp. 568–582.
[28]
François Laroussinie & Kim Guldstrand Larsen (1995): Compositional Model Checking of Real Time Systems. In: 6th International Conference on Concurrency Theory (CONCUR’95), Lecture Notes in Computer Science 962, Springer, pp. 27–41. Available at http://dx.doi.org/10.1007/3-540-60218-6_3.
[29]
Annabelle McIver, Tahiry M. Rabehaja & Georg Struth (2011): On Probabilistic Kleene Algebras, Automata and Simulations. In Harrie C. M. de Swart, editor: 12th International Conference on Relational and Algebraic Methods in Computer Science (RAMICS’11), Lecture Notes in Computer Science 6663, Springer, pp. 264–279. (available at ).
[30]
Mohammad Reza Mousavi, Michel A. Reniers & Jan Friso Groote (2007): SOS formats and meta-theory: 20 years after. Theoretical Computer Science 373(3), pp. 238–272. Available at http://dx.doi.org/10.1016/j.tcs.2006.12.019.
[31]
Cristian Prisacariu (2010): Synchronous Kleene Algebra. The Journal of Logic and Algebraic Programming (JLAP) 79(7), pp. 608–635, doi:10.1016/j.jlap.2010.07.009. (available at ).
[32]
Kenneth Radke, Colin Boyd, Juan Manuel González Nieto & Margot Brereton (2011): Ceremony Analysis: Strengths and Weaknesses. In Jan Camenisch, Simone Fischer-Hübner, Yuko Murayama, Armand Portmann & Carlos Rieder, editors: 26th IFIP-TC-11 International Information Security Conference (SEC), IFIP Advances in Information and Communication Technology 354, Springer, pp. 104–115. Available at http://dx.doi.org/10.1007/978-3-642-21424-0_9.
[33]
Mario Di Raimondo, Rosario Gennaro & Hugo Krawczyk (2005): Secure off-the-record messaging. In Vijay Atluri, Sabrina De Capitani di Vimercati & Roger Dingledine, editors: Proceedings of the 2005 ACM Workshop on Privacy in the Electronic Society, WPES 2005, ACM, pp. 81–89. Available at http://doi.acm.org/10.1145/1102199.1102216.
[34]
Rimvydas Ruksenas, Paul Curzon & Ann Blandford (2008): Modelling and analysing cognitive causes of security breaches. ISSE 4(2), pp. 143–160. Available at http://dx.doi.org/10.1007/s11334-008-0050-7.
[35]
Ryan Stedman, Kayo Yoshida & Ian Goldberg (2008): A User Study of Off-the-record Messaging. In: Proceedings of the 4th Symposium on Usable Privacy and Security, SOUPS ’08, ACM, New York, NY, USA, pp. 95–104, doi:10.1145/1408664.1408678. Available at http://doi.acm.org/10.1145/1408664.1408678.

This document was translated from LATEX by HEVEA.
Made with NvuTry this on Opera browser
©2009-2012 The content of this web site are licenced under the
The condition is to put a visible link to this web site.
Creative Commons License