As a research group, we are actively involved in teaching within the Computer Science degrees at the University of Southern Denmark.
At the undergraduate level, we offer courses within the Computer Science bachelor programme in topics directly related to our research (Concurrent Programming, Programming Languages), as well as the general Introduction to Programming course.
At the graduate level, we offer a course package on Concurrency and Logic within the Master programme in Computer Science. This package includes 4 courses (40 ECTS) and covers the theoretical and practical aspects of designing concurrent and distributed systems, specifying and validating their properties.
Below is a list of the topics we offer for MSc and PhD theses. Many of our proposals can also be developed in the context of company collaborations. You are welcome to contact us to know more about these opportunities.
Topics for MSc theses
Choreographic Programming is a new programming paradigm where programmers write specifications of how concurrent programs should interact, and then a compiler automatically generates code that is guaranteed to be correct and deadlock-free. As a young paradigm, there are a lot of useful and interesting open questions, both on the theoretical and practical levels: efficient and safe programming primitives for concurrent access to shared resources; automatic deployment of code generated from choreographies in cloud environments; specifying and proving safety properties of choreographies (e.g., liveness, security, and privacy properties); integrating choreographic programming with mainstream programming languages and frameworks; exploring the theoretical limits of choreographic programming and its relationship to standard models of computing.
Deployment of sophisticated distributed software applications requires a deep knowledge on the cloud infrastructure and on the application to deploy. For this reasons attempts are developed to simplify and better automate the process of deploying application (DevOps). The goal of this thesis is to enhance and develop tools (e.g., based on machine learning, local search, genetic algorithms, constraint programming) to tackle some of the computational issues for automatizing the deployment of applications in the cloud, and especially the optimization of the resource usage.
Many modern digital systems (as in the Internet of Things, Industry 4.0, and Cloud Computing) are highly concurrent: they carry out multiple activities at the same time and include massive numbers of actors that communicate to exchange data, using multiple CPUs and large-scale networks. Concurrency theory offers solid methodologies to conceptualise these systems, identify problems, and support decision making. Subjects for projects range from pure theory to implementations of theoretical models: quantitative properties of concurrent systems such as availability, efficiency, performance, reliability, robustness, safety, security, survivability, and timeliness; automatic verification of security protocols; new programming approaches for concurrency (e.g., transactional memories); inductive and coinductive proof methods and their applications (e.g., for infinite behaviours, as in service-oriented systems).
When dealing with complex problems (solving big Sudoku puzzles, assign jobs to resources, ...), one of the best possible techniques to use is to combine the strength of a portfolio of available solvers to produce a better unique solver called "portfolio solver". The goal of this thesis is to study new innovative techniques that based on machine learning and heuristics can improve the solving of complex problems, possibly improving even our own gold medals winner solver SUNNY-CP, i.e., one of the best portfolio solver for optimization problems.
Sorting networks are very simple hardware circuits that sort inputs of fixed size n by executing a predetermined sequence of binary compare-and-swap operations. Each operation costs time and energy, and thus it is important to find sorting networks that are as small as possible. However, finding optimal sorting networks is an extremely complex problem that has only been solved for a few small values of n by ingenious combinations of combinatorial techniques, mathematical insights, and clever programming of search algorithms. If you have a background in Mathematics or Computer Science and are looking for a problem that requires a new, creative approach, then this project is for you!
SAT solving tools these days are able to prove unsatisfiability of increasingly large propositional formulas. However, they do so by applying extremely complex algorithms whose correctness it is unfeasible to verify. In order to trust their results, one needs them to output a certificate of unsatisfiability that can be efficiently verified independently. Currently, the languages for such certificates cannot support all the techniques used in SAT solving. The goal of this project is to extend certification languages to cater for hitherto unconvered techniques and develop efficient algorithms for dealing with these extensions.
Do you like (board) games? Have you ever wondered if for a particular game there is a perfect strategy that allows to maximize yours point and possibly win the game? Do you think you have a new and smart way to find good strategies? Then contact us! Working for a thesis may be as fun as playing a game.
If you are interested in doing a PhD in the Concurrency and Logic group, please contact us directly.