Topics

Here is an ongoing chart for the different topics. It is not a flow diagram that will tell you exactly which topic to take, but it gives some ideas of the general topic our group has. If you are really interested in a topic, we might have themes that are available that do not require the full lecture.

We are always happy to hear about other topics (related to our interests however).

Some of our subjects can fit into various topics depending on the approach (for example, hardware verification can be done from the Isabelle side or from the tools side or like a puzzle to verify some properties or as multipliers).

WARNING: the graph below is not complete nor up to date w.r.t. the other chairs. Many chairs are missing like the one of Prof. Schindelhauer. Do not forget to check other chairs when considering a topic!

WARNING2: this graph is regularly updated (see the start point for the current version)

flowchart TD classDef default stroke:#000 classDef bernhard stroke:#f00 classDef mathias stroke:#0f0 classDef tobi stroke:#00f classDef all stroke:#fff classDef bernhard_tobi stroke:#f0f classDef tobiasF stroke:#0ff classDef bernhard_mathias stroke:#770 classDef other_chair fill:#fff,stroke:#333,stroke-width:1px Start["Start (version 4)"]; ML["Machine Learning (ML) + AR"]; MissingSemester["Missing semester
themes
(LSP/emacs/vim/...)"]; Proofs["Writing proofs"]; Bugs["Finding bugs"]; HardwareBugs["bugs in hardware"]; SoftwareBugs["bugs in software"]; TeachingTools["<a href=https://cca.informatik.uni-freiburg.de/software/index.html#teaching-software>Tools for teaching</a>
(like <a href=https://cca.informatik.uni-freiburg.de/grs-bits/>GRS</a>)"]; Isabelle["<a href=https://cca.informatik.uni-freiburg.de/fleury/projects.html>Isabelle formalization</a>"]; Algorithms["Maybe the chairs of
Profs. <a href=https://ad.informatik.uni-freiburg.de/>Bast</a> or <a href=https://ac.informatik.uni-freiburg.de/>Kuhn</a>
fit better?"] Tools["Developing tools
for verification"]; MLTraining["Using AR
for training"]; MLTrainingAR["Training on
AR papers"]; MLIsabelle["Using ML in
Isabelle"]; DevelopTools["Developing tools"]; UsingTools["Using tools"] ARTools["SAT solving,
SAT variants (#SAT, ...),
MaxSAT, BDDs"]; IsabelleTools["<a href=https://cca.informatik.uni-freiburg.de/fleury/projects.html>Isabelle+
SMT solving</a>"]; Multipliers["Multipliers"]; CompareTools["Tool Comparison
(like models)"]; Scholl["Maybe the chair
of <a href=https://abs.informatik.uni-freiburg.de/src/team.php>Prof. Scholl</a>?"]; Scholl2["Maybe the chair
of <a href=https://abs.informatik.uni-freiburg.de/src/team.php>Prof. Scholl</a>?"]; Scale4Edge["<a href=https://ira.informatik.uni-freiburg.de/src/projects_tfi.php?projectId=11896>Scale4Edge project</a>"]; ARSAT["SAT solving
implementation or theory
or performance analysis
(like <a href=https://cca.informatik.uni-freiburg.de/papers/PolittFleuryBiere-MBMV23.pdf>this</a>)"]; ARSATProof["SAT proof checking"]; ARMaxSAT["<a href=https://cca.informatik.uni-freiburg.de/teaching/project-and-thesis.html#maxsat-solving>MaxSAT solving</a>"]; Heuristics["Visualization of
the solver's work (like <a href=https://www.youtube.com/watch?v=MOjhFywLre8>this</a>)"]; Puzzles["<a href=https://cca.informatik.uni-freiburg.de/teaching/project-and-thesis.html#representing-a-puzzle-and-solving-it>Representing a puzzle</a> and
solving it with
SAT/MaxSAT/SMT/...
(like str8ts)"]; FuzzingDD["Fuzzing and
delta-debugging"]; OtherPath1["Maybe the chairs of
Profs <a href=https://swt.informatik.uni-freiburg.de/>Podelski</a> or
<a href=http://proglang.informatik.uni-freiburg.de/teaching/themen.html>Thiemann</a>
fit better?"]; OtherPath2["Maybe <a href=https://www.ai.uni-freiburg.de/de/frai-personen>another ML chair</a>
fits better?"]; Start --> ML; Start --> Proofs; Start --> Bugs; Start -- Bachelor Project(?),
few ideas for now --> MissingSemester; Start -- Bachelor Project --> TeachingTools Proofs -- by hand
project (learn) +
thesis --> Isabelle; Proofs -- using a tool --> Tools; Proofs -- I do not want tools
I want LaTeX --> Algorithms; Tools -- yes --> DevelopTools; Tools -- not really --> UsingTools; DevelopTools -- yes --> ARTools; DevelopTools -- interface between tools --> IsabelleTools; DevelopTools -- brand new tools,
master level
requires arithmetics --> Multipliers; DevelopTools --> CompareTools; DevelopTools --> Scholl2; Bugs --> HardwareBugs; Bugs --> SoftwareBugs; ARTools -- requires
SAT lecture
every SS --> ARSAT; ARTools --> ARSATProof; ARTools --> ARMaxSAT; ARTools -- no too much about internals,
Bachelor level --> Heuristics; UsingTools -- Bachelor Project --> Puzzles; SoftwareBugs -- requires
Debugging and
Fuzzing lecture
every WS --> FuzzingDD; SoftwareBugs --> OtherPath1; HardwareBugs -- hardware
parts --> Scholl; HardwareBugs -- full CPU hardware --> Scale4Edge; ML -- but I do not like
automated reasoning? --> OtherPath2; ML --> MLTraining; ML -- Bachelor --> MLTrainingAR; ML -- Bachelor --> MLIsabelle; class ARMaxSAT tobi class Isabelle,IsabelleTools,Multipliers mathias class ML,MLTraining,MLIsabelle bernhard class ARSAT,Puzzle,MissingSemester,Heuristics,CompareTools,Puzzles,TeachingTools all class FuzzingDD bernhard_tobi class OtherPath1,OtherPath2,Scholl,Scholl2,Algorithms other_chair class Scale4Edge tobiasF class MLTrainingAR,MLIsabelle bernhard_mathias

The caption and the co-supervisor is given by the stroke around the box:

flowchart TD classDef bernhard stroke:#f00 classDef mathias stroke:#0f0 classDef tobiasF stroke:#0ff classDef tobi stroke:#00f classDef all stroke:#fff classDef bernhard_tobi stroke:#f0f classDef bernhard_mathias stroke:#770 Supervision["Supervision caption
(Armin Biere always involved)"]; Bernhard["Bernhard Gstrein"]; Mathias["Mathias Fleury"]; Tobias["Tobias Paxian"]; TobiasF["Tobias Faller
partially independent
of the chair"]; All["Anyone in the group
depending on the exact topic"]; Bernhard_Tobi["Bernhard Gstrein or Tobias Paxian"]; Bernhard_Mathias["Bernhard Gstrein and
Mathias Fleury"]; Supervision --> Bernhard; Supervision --> Mathias; Supervision --> Tobias; Supervision --> TobiasF; Supervision --> All; Supervision --> Bernhard_Tobi; Supervision --> Bernhard_Mathias; class Tobias tobi; class Mathias mathias; class Bernhard bernhard; class TobiasF tobiasF; class All all; class Bernhard_Tobi bernhard_tobi; class Bernhard_Mathias bernhard_mathias;

Process to register a project and define the goals

General flow to get a project:

You send an email to Armin and get a meeting (mostly online nowadays). In this email you should include: (i) what you are currently studying (ESE / CS / …); (ii) which lectures you heard from us and which you are currently hearing; (iii) what you are interested in (bachelor/master and project/thesis); and (iv) if you are an ESE student, make sure to add if you did you Bachelor in Freiburg (and include relevant information like whether you know verilog)
You look at the chart above and find 2-3 topics that interest you most.
You meet with us now and tell us which topics you are the most interested in. This is also the right moment to tell us if you have favorite topics. We discuss several subjects for each topic (using a list that we do not publish). If you are interested in Scale4Edge, then you need an meeting organized by Tobias Faller.
We assign you a group member (the co-supervisor, not Armin) and a deadline (usually 2 weeks)
Before the deadline you tell the co-supervisor which topic you picked or if you gave up
You register with Frau Moses (see full description here) by putting the group member in CC with a deadline (end of semester) / You fill the form and we meet
We can meet for the first time: Discuss potential milestones (usually 3 + a presentation/writing of the thesis; the first milestone decides if you pass or not)
Second meeting: you write the milestones properly down by email and you start

Some more detailed on topics

We below give some more details in order to make it easier for you to imagine what the topic can look like. This is not a real subject, but should give ideas what to expect.

Representing a puzzle and solving it

The objective of these projects is to encode a game/puzzle and solve it.

Good options for this include games:

with complete information (you know the position of every piece)
with a reasonably small game state (no, you will not solve Go or chess with a SAT solver)
that are not part of Yurichev’s book or have not been solved in the exact same way.

A great example would be Sudoku, although it has already been solved countless times with a SAT solver and it is a bit too easy (just search for it on the internet).

Your task involves:

Selecting a game, preferably one you enjoy.
Encoding the game.
Translating the solution back into a format that can be checked. For instance, you may want to represent a solution and verify it.
Depending on the project, determine some numbers: if you’re working on Mastermind, for example, you might be interested in the average number of solving steps (to compare it with other approaches); how many different solutions exist under the given constraints?

Thilo Langensteiner worked on Ubongo 3D. He solved it using his own encoding and visualized the game to check the solutions. Despite the challenge, he still enjoyed the game at the end of the project.

MaxSAT solving

Many topics are possible, but here is a general description of one that was already given.

The goal is to modify part of the translation into an SAT Solver (like the adder used to represent weights - SAT solvers do not understand numbers, so you need to encode the question).

While there are no prerequisites, you should enjoy coding and debugging in C++. Additionally, as you will also spend time on propositional logic, you should also find it enjoyable.

Teaching tools