Meet our PhD students

At the Department of Computer Science, we have a lot of talented PhD students in our various research groups. Here, you can find information about some of those we have sent out in to the world, their research projects and where their PhD degree has taken them.

Interested in becoming a Phd at CS? Find more information here.

Already, graduated from CS? Then become a member of our Alumni network at LinkedIn.

Cryptography and security

The Hitchhiker’s Guide to Garbled Circuits – Garbled Circuits and Their Applications to Maliciously Secure Two-Party Protocols

Tore Kasper Frederiksen. PhD defense, 29 October 2015.

Using encrypted circuits to efficiently enforce honesty on the Internet
During his PhD studies, Tore Kasper Frederiksen researched the cryptographic primitive – garbled circuits. Garbled circuits can be seen as an encryption of an ordinary circuit. They are extremely powerful primitives that can allow two mutually distrusting people to compute any program where they each have some secret input and each should learn some secret output. In fact, this is possible even in the case where one of the people is running rogue software!

Tore Kasper Frederiksen studied how to improve the efficiency of this primitive to move it closer to real-world usage. For example, to make it possible for you to give sensitive information as input to a program running with an untrusted Internet service, without fear of this service actually learning your sensitive information.

The research findings include a new type of garbled circuits – more efficient than previous constructions – which can be used in certain settings. Furthermore, the findings include theoretical and practical improvements of the common protocols using garbled circuits.


Title of dissertation: The Hitchhiker’s Guide to Garbled Circuits – Garbled Circuits and Their Applications to Maliciously Secure Two-Party Protocols

Supervisor: Jesper Buus Nielsen

Contact information: Tore Kasper Frederiksen, +45 2327 7762

Now works at: Cryptomatic

Data-intensive systems

Multi-Criteria Decision Support Queries in Exploratory & Open World Settings

Michael Lind Mortensen. PhD defence, 29 January 2016.

When presented with a multitude of options to choose from (e.g., houses, cars, hotels, etc.), filtering those options to find the most interesting is an all too common and time-consuming task for normal users.

During his studies, Michael investigated how to alleviate some of this filtering burden through so-called multi-criteria decision support queries. These methods take the initial set of options and filter them into a smaller, more manageable, set that captures the preferences of users. Historically these techniques have been ill-suited for real users and real world contexts, either being ignorant to how users learn about their options or being unable to actually adapt to the real-world preferences of users.

Michael’s research findings have contributed to bringing these techniques closer to real world application, introducing both techniques for supporting the user in exploring their options efficiently, as well as techniques for adapting multi-criteria filtering to the open world; i.e., the real, ever-expanding, and unknown world in which users actually make decisions, rather than the limited closed-world model defined by our database.

The PhD degree was completed as part of the Data-Intensive Systems group at the Department of Computer Science, Aarhus University. Part of the work was done while at Brown University, Providence, RI, USA.


Title of dissertation: Multi-Criteria Decision Support Queries in Exploratory & Open World Settings

Supervisor: Ira Assent

Contact information: Michael Lind Mortensen, tel.: +45 50 53 21 65

Now works at: Netcompany A/S

Logic and semantics

On semantics and applications of guarded recursion

Aleš Bizjak. PhD defence, 15 April 2016.

 

Semantics and applications of guarded recursion.

 

In mathematics and computer science, it is often necessary to describe objects in a self-referential way. Guarded recursion is a way of ensuring that self-referential descriptions describe unique objects.

In the first part of his dissertation, Aleš Bizjak studied the semantics of programming languages with features such as non-deterministic and probabilistic choice, polymorphism and local state. These are difficult to reason about, especially in combination, and guarded recursion provides a simple solution to some of the challenges.

In the second part of his dissertation, Aleš Bizjak studied the semantic foundations for type theories with a special ‘later’ modality, which is used to guard self-references in recursive definitions. The semantic foundations ensure that the type theories are consistent, which roughly means that they cannot be used to construct things we do not want. These semantic foundations were used in the design of a type theory, the purpose of which is to aid in the construction of models of programming languages, such as the ones considered in the first part of the dissertation. The description of this type theory forms the final part of the dissertation.

The PhD degree was completed at the Department of Computer Science, Science and Technology, Aarhus University.

Title of dissertation: On semantics and applications of guarded recursionSupervisor: Lars Birkedal

Contact information: Aleš Bizjak, abizjak@cs.au.dk, +45 8715 6158

Now works at: Aarhus University

Madalgo / Algorithms and data structures

Space Efficient Data Structures and External Terrain Algorithm

Jakob Truelsen. PhD defense, 17 April 2015.

Handling large data sets – use as little space as possible or use the disk.
During his PhD studies, Jakob Truelsen looked into handling large data sets that are on the limits of what can be handled in the memory of a regular computer.

He studied how to minimize the space usage of different data structures, so that more data can be processed using less memory. He also investigated how to efficiently use the hard disk when data does not fit in memory. Here he devised an algorithm to efficiently generate and simplify contour maps for large data sets.

The PhD degree was completed at MADALGO, Department of Computer Science, Science and Technology, Aarhus University.


Title of dissertation: Space Efficient Data Structures and External Terrain Algorithm

Supervisor: Gerth S. Brodal

Contact information: Jakob Truelsen, jakobt@cs.au.dk, +45 3028 4083

Handling massive and dynamic terrain data

Morten Revsbæk. PhD defence, 14 November 2014.

Handling massive and dynamic terrain data – automatic production and maintenance of precise flood risk maps and nautical charts.
Recent technological advances within laser and sonar technology have greatly increased our ability to create detailed digital models representing the surface of the Earth, both below and above the ocean. For example, the Danish authorities are currently undertaking a nationwide survey where surface elevation is measured using advanced laser technology. This survey will result in a nationwide digital surface model containing a measurement for every 0.5 metre across the entire country or approximately 170 billion measurement points in total. Using this digital model, where the garden of a standard family home contains thousands of measurements, it is in principle possible to perform topographic analyses such as flood risk analyses in a detail that far exceeds anything seen before. However, these detailed digital surface models represent massive amounts of data that is difficult or even impossible to process using standard algorithms or software.

In his PhD dissertation, Morten Revsbæk describes I/O-efficient algorithms for the efficient analysis of massive surface models. He focuses on algorithms for mapping flood risk and the automatic production of precise contour maps for creating nautical charts, for example. He also presents fundamental results for how to maintain these maps efficiently as the surface model changes over time.

The PhD degree was completed at the Department of Computer Science, Science and Technology, Aarhus University.


Title of dissertation: Handling Massive and Dynamic Terrain Data

Supervisor: Lars Arge

Contact information: Morten Revsbæk, mrevsen@gmail.com

Now works at: SCALGO

Mathematical computer science

On the Combinatorics of SAT and the Complexity of Planar Problems

Navid Talebanfard. PhD defense, 17 November 2014.

Structure of solution spaces of logical equations and complexity of planar graph problems.
During his PhD studies, Navid Talebanfard investigated different aspects of the Boolean satisfiability problem. With his collaborators, he constructed very hard instances of PPSZ and DPLL algorithms, providing evidence for the strong exponential time hypothesis (SETH).

Navid Talebanfard also developed techniques to gain more insight into the structure of the solution spaces of Boolean formulae. In another part of his work, he and his co-authors applied algebraic techniques to prove upper bounds of the complexity of several problems associated with planar graphs.

The PhD degree was completed at the Department of Computer Science, Science and Technology, Aarhus University.


Title of dissertation: On the Combinatorics of SAT and the Complexity of Planar Problems

Supervisor: Peter Bro Miltersen

Now works at: Saarland University

Social Welfare in Algorithmic Mechanism Design Without Money

Aris Filos-Ratsikas. PhD defence, 5 August 2015.

Algorithmic mechanism design: how to get selfish people to make socially acceptable decisions.
During his PhD studies, Aris Filos-Ratsikas researched the topic of social welfare maximisation in algorithmic mechanism design settings without money. In such settings, a group of participants who are solely concerned with their own well-being are asked to make a collective decision. Specifically, they are asked to specify the intensity of their preferences over a set of possible outcomes (such as who to elect for president or where to build a library on a street). A central planner – the designer – subsequently implements some function of the specified preferences. Since people are selfish, it is quite possible that they might misreport their preferences in order to manipulate the outcomes.

Aris Filos-Ratsikas studied the impact of this strategic behaviour of the participants on the social welfare of the system – or ways to prevent it from happening. The social welfare is the aggregate utility or happiness of people for the outcome of the system. The research for his dissertation is concerned with the fundamental problems of voting and resource allocation and the design and analysis of mechanisms that achieve good levels of social welfare in the worst case. His results incorporate techniques from mechanism design, game theory and combinatorial optimisation.

The PhD degree was completed at the Department of Computer Science, Science and Technology, Aarhus University.


Title of dissertation: Social Welfare in Algorithmic Mechanism Design Without Money

Supervisor: Peter Bro Miltersen

Contact information: Aris Filos-Ratsikas, +45 6151 7947

Now works at: University of Oxford

Ubiquitous computing and interaction

Changing the shape of interaction – shape-changing interfaces

Majken Kirkegård Rasmussen. PhD defense, 2 September 2015.

Designing digital qualities in physical artefacts – exploring shape-changing interfaces
Design prototype: CoMotion, a shape-changing bench designed to investigate how people experience and make sense of shape-changing interfaces in context, as well as how atmosphere and context affect the experience of shape change. See video here.

During her PhD studies, Majken Kirkegård Rasmussen conducted research into shape-changing interfaces. These can briefly be described as interfaces that are capable of changing their physical form through digitally controlled actuation. Shape-changing interfaces focus on blending the dynamic qualities of the digital world with the tactile qualities of the physical one, creating interfaces that have the potential to adapt their shape to suit different users, usages, purposes and contexts. The overarching research approach was design, where Majken Kirkegård Rasmussen used design cases to explore and develop theoretical and practical knowledge.

The research contributes by providing frameworks and terminology for shape-changing interfaces, novel design concepts, and insights into how people experience shape-changing interfaces.

The PhD degree was completed at the Department of Computer Science, Science and Technology, Aarhus University.


Title of dissertation: Changing the shape of interaction – shape-changing interfaces

Supervisor: Marianne Graves Petersen

Contact information: Majken Kirkegård Rasmussen, +45 4062 0343

Interactive Visual Analytics of Big Data – A Web-Based Approach

Matthias Nielsen. PhD defence, 20 April 2016.

 

Apprehensible Interactive Visual Analysis of Big Data in Web-Browsers.

 

During his studies, Matthias Nielsen researched how internet browsers can be used for enabling professional and private non-programmer users to perform exploratory visual analysis of Big Data. Traditionally, exploratory visual analysis of Big Data has been confined to extensive software suites and has been performed by expert users. To improve this, Matthias Nielsen has developed new apprehensible visual representation for visualizing large datasets. Furthermore, he has described and documented techniques for efficiently visualizing large datasets in internet browsers. Lastly, he has developed new ways of using input from touch-screens to interact with data interactive data visualizations. Together, these contributions advance facilitating visual data analysis for non-programmer users by enabling apprehensible interactive visual analysis of large datasets in internet browsers.

The PhD degree was completed at the Ubiquitous Computing and Interaction Group, Department of Computer Science, Science and Technology, Aarhus University.

Title of dissertation: Interactive Visual Analytics of Big Data – A Web-Based Approach

Supervisor: Kaj Grønbæk

Contact information: Matthias Nielsen, e-mail: mail@matthiasnielsen.dk, tel.: +45 20 65 13 16

Now works at: Alexandra Instituttet

Programming languages

On Computational Small Steps and Big Steps: Refocusing for Outermost Reduction

Jacob Johannsen. PhD defense, 13 March 2015.

Flexible and consistent reasoning in programming languages.
Three examples of semantic specifications for subtraction. The image shows how subtraction can be specified using different semantic styles: natural semantics, denotational semantics in continuation-passing style, and a state-transition system. Do the three specifications define the same behavior for subtraction? In his PhD project, Jacob Johannsen studied how such specifications can be mechanically derived from each other, and how derivational techniques can be applied to a new class of programming languages.

Just like natural languages, programming languages have a syntax and a semantics. This semantics is specified mathematically, and lets us reason formally about programs. There are several standardized ways to specify a semantics, and each of them is useful for some but not all types of reasoning. However, it is non-trivial to determine whether two semantic specifications are equivalent, i.e. whether they specify the same behavior.

During his PhD studies, Jacob Johannsen researched techniques to mechanically derive equivalent semantic specifications enabling flexible and consistent reasoning, and how existing derivational techniques can be extended to deal with new classes of problems both within and outside programming languages.

The PhD degree was completed at the Department of Computer Science, Science and Technology, Aarhus University.


Title of dissertation: On Computational Small Steps and Big Steps: Refocusing for Outermost Reduction

Supervisor: Olivier Danvy

Contact information: Jacob Johannsen, +45 2386 2485

Now works at: Semmle

Automated Testing of Event-Driven Applications

Casper Svenning Jensen. PhD defense, 9 March 2015.

Automated testing of event-driven applications.
Event-driven applications such as web applications and Android mobile applications can be tested by selecting interesting inputs (i.e. sequences of events) and deciding whether they lead to failures when applied to the event-driven applications. Automated testing promises to reduce the workload for developers by automating the process of selecting interesting inputs and detecting failures. However, it is non-trivial to conduct automated testing of event-driven applications because of infinite input spaces, for example, and the absence of specifications of correct application behavior.

In his research, Casper Svenning Jensen identified a number of challenges when conducting automated testing of event-driven applications, and he proposes a number of techniques for solving these challenges.

The PhD degree was completed at the Department of Computer Science, Science and Technology, Aarhus University.


Title of dissertation: Automated Testing of Event-Driven Applications

Supervisor: Anders Møller

Contact information: Casper Svenning Jensen, +45 4292 6287

Now works at: Uber

Pointer Analysis for JavaScript Programming Tools

Asger Feldthaus. PhD defence, 9 January 2015.

Programming tools for JavaScript using static analysis.
Programming is a difficult discipline and occasionally requires much ingenuity from the programmer. However, the programmer is also faced with many arduous, time-consuming tasks, such as restructuring the source code or looking up documentation. Programming tools are often used to simplify and automate such tasks.

JavaScript is a widely used programming language and is the only language understood by all major web browsers. However, the dynamic nature of JavaScript has led to a lower standard of programming tools compared with other languages, especially statically typed languages such as Java and C#.

In his research, Asger Feldthaus shows how various static analysis techniques can be used to make more powerful programming tools for the JavaScript language. This can help programmers who wish to develop software in the native language of the web, while also reaping some of the benefits traditionally reserved for statically typed languages.

The PhD degree was completed at the Department of Computer Science, Science and Technology, Aarhus University.


Title of dissertation: Pointer Analysis for JavaScript Programming Tools

Supervisor: Anders Møller


Designing abstractions for JavaScript program analysis

Esben Andreasen. PhD defence, 24. August 2016.

 

Analysis of JavaScript programs.
During his PhD studies, Esben Andreasen researched the use of program analysis for programs written in the JavaScript programming language. Program analyses, such as dataflow analyses and type systems, can be used to guarantee behaviors of programs. A classic guarantee of interest is that analyzed programs do not crash; more technical guarantees can be used to optimize analyzed programs.


JavaScript is a widely used programming language, famously used for creating interactive web pages. However, programmers code JavaScript programs in so complex ways that program analyses often give up when trying to reason about them. Program analyses for other programming languages, e.g. Java, are often more useful since they are analyzing relatively simpler programs.

In his research, Esben Andreasen shows how various program analyses can be designed and improved to reason more precisely about real-world JavaScript programs.

The PhD degree was completed at the Department of Computer Science, Science and Technology, Aarhus University.

Title of dissertation: Designing abstractions for JavaScript program analysis

Supervisor: Anders Møller

Contact information: Esben Andreasen esbena@cs.au.dk

Now works at: Aarhus University

 

Type Soundness in the Dart Programming Language

Fabio Strocco. PhD defence, 8 September 2016.

Type Systems and Program Analysis for the Dart Programming Language.
During his studies, Fabio Strocco researched novel type systems and program analysis techniques for Dart. Dart is a programming language designed by Google to develop for the web, the mobile and the Internet of Things. The language was presented for the first time at the GOTO conference in Aarhus, in 2011.

Fabio Strocco built a mathematical model of Dart to use as a foundation for investigating some
of the most controversial language design choices. He discovered that small reasonable changes of the
specification can provably give more guarantees on programs' behavior and showed experimentally that some of these changes would not hinder programmers.


Fabio Strocco designed and implemented a novel technique to find errors in existing Dart programs,
which has been shown to be effective on a large set of Dart projects. Together, these contributions can drive future language design choices and improve tool support for Dart and similar programming languages.

The PhD degree was completed at the Programming Languages group, Departement of Computer Science,
Science and Technology, Aarhus University.

__________________________________

Title of dissertation: Type Soundness in the Dart Programming Language

Supervisor: Anders Møller

Contact information: Fabio Strocco, e-mail:fabiostrocco@gmail.com, tel.: +45 42 56 26 38

Now works at: Microsoft