PhD theses

Name Title of the PhD thesis at
Gianluca Turin Exploiting Abstract Data-Access Patterms for Better Data Locality in Parallel Processing UiO
Farzane Karami Language-based Approaches for Enforcing Privacy and Security Policies UiO
Daniel Fava Relaxed Memory Models and Data-Race Detection tailored for Shared-Memory Message-Passing Systems UiO
Shukun Tokas Analysis and Enforcement of {GDPR}-related Privacy Principles in Object-Oriented Distributed Systems UiO
Bjørnar Luteberget Automated Reasoning for Planning Railway Infrastructure UiO
Johanna Beate Stumpf Virtually Timed Ambients: A Calculus for Resource Management in Cloud Computing UiO
Violet Ka I Pun Behavioural Static Analysis for Deadlock Checking UiO
Silvia Lizeth Tapia Tarifa Executable Modeling Deployment Decisions for Resource-Aware Distributed Applications UiO
Thi Mai Thuong Tran Compositional Formal Analysis for Concurrent Object-Oriented Languages UiO
Arild B. Torjusen Specification-Based Verification and Testing of Open Distributed Systems UiO
Erika Ábrahám An Assertional Proof System for Multithreaded Java - Theory and Tool Support U. Leiden
Andreas Grüner Testing Concurrent Objects U. Leiden
Immo Grabe Static Analysis of Unbounded Structures in Object-Oriented Programs” U. Leiden

Opponent / Examinor / Defense committee member / adjudication of PhD theses

Name Title of the PhD thesis defended at
André Büttner (working title) UiO
Marta Różańska Utility Based Optimization Of Cloud Application Resources UiO
Tamas Bisztray Investigating Privacy Aspects of Identity Management: From Data Protection Impact Assessment for Biometric Applications to Privacy-Centric Password Testing UiO
Kai Arne Schröder Myklebust Ecotoxicological Effect Prediction using a Tailored Knowledge Graph UiO
Johanna Johansen Towards Making Privacy Usable UiO
Francisco Ramón (Kiko) Fernández Reyes Abstractions to Control the Future U. Uppsala
Hendrik Maarand Operational Semantics of Weak Sequential Composition Tallinn U. of Technology
Seray Fayyad Measurable Security for Systems Built upon Internet of Things UiO
Muhammad Zohaib Zafar Iqbal Environment Model-Based System Testing of Real-Time Systems UiO
Rudolf Schlatte Passive Testing with Parallel Object-Oriented Software Models U. Graz
Joachim Klein Compositional Synthesis and Most General Controllers TU Dresden
Ingrid Yu Type Safety for Distributed, Concurrent Programs with Class Upgrades UiO
Xuedon Liang QoS Provisioning for Wireless Sensor Networks: Algorithms, Protocols and Modeling UiO
Anders Moen Hagalisletto Automated support for the design and analysis of security protocols UiO

Third semester evaluation

Name year
Åsmund Aqissiaq Arild Kløvstad 2024
Malte Hansen 2023
Tobias John 2023
Chinmayi Prabhu Baramashetru 2022
Mateusz Zych 2022
Robert Chetwyn 2022
Andre Büttner 2022
Johanna Johansen 2020
Marius Gaute 2020
Daniel Bakkelund 2018

Master thesis supervision

See also the extra webpages for completed and for ongoing theses for more information for some of the theses


Name Title of the thesis
Mohamed Hocein el Morabeti Developing a Verification Tool for Concurrent Software in Modern Programming Languages (working title)
Sean Amaury Lapalus A Domain-Specific Language for Real-Estate Floor Plans (working title)
Jakob Konrad Hansen  
Jakub Wasylków Verification software for concurrent software written in C using GCD (working title)
Saima Sultana A comparative analysis of the impact of different SSD tools and methods on software development productivity
Sebastian Max Sjøvoll Kingston Automated Refactoring of Test Suites in Python
Nemanja Lakicevic Runtime verification with Linux BPF

Finished (including also ``study-theses’’ and diploma theses (Diplomarbeiten and Studienarbeiten))

Name Title of the thesis
Audun Wolden Exploring Automated Parallellization of Loops in Go
Sondre Åge Godø Teigen A Relaxed Memory Model Based On Message Passing and Delayed Evaluation of Shared Memory Operations
Sarek Skotåm CreuSAT. Using Rust and Creusot to create the world’s fastest deductively verified SAT solver
Rasmus Drønnen Pre-Filling Orleans grains for market data analysis
Asbjørn Gaarde Compile-Time Reflection in Rust. A New Tool for Making Derive Macros
Henrik Klev Verifying EVA. Formal Verification of the software deciding Norwegian governmental elections
Anna Katharina Wickert Information Flow analysis in Go
Per Ove Ringdal Automated Refactoring of Rust Programs. Algorithms and implementations of Extract Method and Box Field
Araz Abishov Efficient Persistent Vector Implementation for Rust
Christopher Trotter A Non-Sculpting Theorem in Non-Interleaving Models for Concurrency
Morten Aske Kolstad Verification of Haskell programs with Liquid Haskell
Ratan Bhadur Thapa Partially Ordered Sets with Interfaces: A Novel Algebraic Approach to Concurrrency
Yrjan Skrimstad Improving Trust in Compilation through Reproducible Builds and Diverse Double Compilation
Tor Husaboe A Comparative Evaluation of the New C++ Standard
Pavel Jurasek PHPWander: a Static Vulnerability Analysis Tool for PHP
Håkon Smørvik Comparative study of modern programming languages and frameworks for web services (announcement)
Eric Vesteraas Rust Types from JSON samples
Altin Qeriqi A PLC-NuSMV Compiler for Model Checking Safety Critical Control Systems
Stian Valle Shared Variables in Go. A Semantic Analysis of the Go Memory Model
Carl Martin Rosenberg Leveraging DTrace for Runtime Verification
Lars Tveito Developing Real-Time Collaborative Editing Using Formal Methods
Olaf Aarseth Berge A Survey of JavaScript Features
Christian Bergum Bergersen Detection of Bugs and Code Smells for the Go Programming Language
Joakim Kristiansen Safer Refactorings
Peter Brottveit Bock Formalization of a type and effect system using Coq and OTT
Immo Grabe Cloning and Processes
Immo Grabe Konzept und Implementierung einer Datenbankanwendung für einen medizinischen Diagnosekatalog (Studienarbeit)
Michael Harder On Specification and Bounded Reachability of Linear Hybrid Systems (Studenarbeit)
Claus Traulsen Enumerative model checking using constraints for asynchronous systems with queues
Andreas Grüner Cliques and components: Implementing traces and object connectivity for a concurrent language
Thomas Richter Komponentenbasierter Entwurf und Spezifikation eines Softwareprojektes mittels UML and Java 2 Enterprise Edition
Mike Scheske Software Engineering im SAP R/3
Tim D’Avis Verification of dynamically chaning asynchronous networks
Tim D’Avis Verifikationsfallstudie für nebenläufiges Java (Studienarbeit)
Henrik Bohnenkamp CLOWN: Concurrent Language with Objects and Wait-by-necessity (Studienarbeit)
Magnus Binder Modelling von guarded choice in Pict
Christoph Wedler Verifikation objektorientierter verteilter Systeme
Wolfgang Naraschewski Object-oriented proof principles using the proof-assistant LEGO
Michael Egner Korrekter Entwurf objektorientierter Verteiler Programme durch Programmtransformation
Thomas Schreiber/Kleymann Verifikation von imperativen Programmen mit dem Beweisprüfer LEGO

Opponent for master defenses

Name title
Nasir Abdi Awed Towards integrating static code analysis and hybrid fuzzing for more efficient bug detection
Krishant Pokharel Agile and Secure Softwre Development. An extension of XP to build secure software
Marlen Jarholt Frog: Functions for ontologies. An extension for the OTTR-framework
Namrah Azam Attack scenarios on AMI that Compromise Human Behaviour and Cellular Networks
Fredrik Rømming Learning to Reason
Anastasia Orishchenko Towards Safety Standard Compliance of IoT Software Systems Using Modelling and Verification with DCR Graphs
Anders Jakob Sivesind Community Coordinated Artificial Intelligence. Towards a unified framework for the democratisation of AI
Ugur Bayram Semantic Attribute-based Access Control. Developing an Access Control solution for IoT Gateways applied to Smart Home Care
Benjamin Oliver Equality Preprocessing in Connection Calculi
Kudakwashe Chambwe Model-based Secure Software Engineering using UMLsec applied to Assisted Living and Home Care
Manoj Upadhaya Process Modelling Based on Smart Home System Using JBoss
Subhash Neupane Modeling Smart Home Processes unsing the Event-Based Modelling Language Tools of DCR graph
Sigurd Kittilsen Partitioning {0,1,…,r} into m subsets of equal sum
Aulon Mujaj A comparison of secure messaging protocols and implementation
Lars Kristian Maron Telle An Exploration into Goodstein Sequences and Hydra Games
Andreas R. Askeland Investigations in complexity theory related to the space hierarchy problem
Simen Heggestøl Visual Query formulation and subclass reasoning for linked open data
Marius Standhaug An R2RML mapping management API in Java
Wenlu Zhang Formal moddeling and analysis of the CANopen protocol in full Maude