Topics for the seminar
Below are topics that we can directly supervise during this seminar. We also allow other topics if you have your own supervisor who is willing to evaluate your writing for this seminar.
- How Amazon Web Services Uses Formal Methods. For this topic, you should look into the methods Amazon used to verify some aspects of their web service design. The method they used was developed at Microsoft Research: TLA+ homepage. This topic could be approached in various ways. I would be interested in both basic overviews to popularize these methods here in Estonia as well as more in-depth descriptions of the tools and the theory behind it.
- Static Race Detection for Device Drivers: The Goblint Approach. Gobint is a static analyzer that we develop together with the Technical University of Munich. Although Goblint is already the best static race detection tool around, it's still somewhat useless for end users. During this term, we will be pushing towards a useful analyzer, exploring differential verification, counter-example generation (learning from the CPAchecker) and apply statistical methods to rank warnings. In this case, we will even write parts of the paper for you, but there are many things you can do to help. If you learn to develop the analyzer, the Munich team have well-funded Ph.D. positions to offer.
- Help students learn programming with Thonny. The best python IDE for learning to program in python is developed here in Tartu. Many students have contributed to this, but there is still plenty to do: topics (Estonian). The project is now in such a stage that you could also look into program analysis and synthesis techniques to, e.g., provide better feedback to students.
- Optimizing the protocols of maliciously secure Sharemind. This is a language-based security topic, but it essentially boils down to doing some graph transformations. There is more details about this in the crypto seminar. With their SecreC language, Cyber is doing some of the most interesting programming language research in Estonia. This topic is highly recommended for people interested in language-based security.
- Post-Rebel Dynamic Software Update. The most successful commercial tool for dynamic reloading of Java classes is ZeroTurnaround's JRebel. Are there any academic developments in reloading since then? This is a good topic if you are also taking their course on Java Fundamentals and find Java technology interesting.
- Back to Basics with Conjugate Hylos. In Tartu's golden age of programming language research, before Jevgeni Kabanov went off founding ZeroTurnaround, he created a recursion scheme for dynamic programming, the dynamorphism. Almost ten years later, Oxford researchers have generalised this line of work, culminating in the Mother of All Recursion Schemes. Find out who this mother is and maybe you might create the next big Estonian Start-Up. (Obviously joking, but then, this is also the trajectory of Eric Meijjer, so who knows...)
- Real World Haskell. For students taking our programming languages course or just interested in functional programming, you could look at some advanced features of Haskell, such as monad transformers, and write a brief account of what it is good for. Alternatively, you could look at practical uses of functional programming; for example, I would be interested in a down-to-earth buzzword-free description of the Lightbend Reactive Platform.
- Verified Programming with Dafny. Verified programming is the future of programming. There are different approaches to this, such as Agda2, Coq, F*, but Dafny has a simple tutorial on Rise4Fun. Here, you could write your own account of attempting to verify a small program. We will help you select a good example based on existing tutorials. You don't necessarily have to succeed with the proof in order to complete the writing.
- How does Excel's Flash Fill feature work? This is an example of program synthesis, particularly Program by Example (PBE). There are many other choices in this area. Have a look at Summit Gulwani's page on program synthesis. You could write a very general overview of the field of program synthesis or focus on a single application and explain how it works.
- Plumbr: Dynamic Analysis & Monitoring. I would like to offer a topic from this company as well, but haven't yet synchronized with them. Let me know if someone is very interested in dynamic analysis, monitoring or profiling. You can also look at some more academic work in this area, such as DiSL, or consider "runtime verification", such as JUnitRV.
You are naturally welcome to discuss your own topic ideas. I'm generally interested in all work published in ACM SIGPLAN conferences. To get an idea of this field, you may have a look at this list of papers featured as CACM research highlights.