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)
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"]; 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
(like <a href=https://cca.informatik.uni-freiburg.de/papers/PolittFleuryBiere-MBMV23.pdf>this</a>)"]; 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 --> 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; class ARMaxSAT tobi class Isabelle,IsabelleTools,Multipliers mathias class ML,MLTraining 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
The caption and the co-supervisor is given by the stroke around the box:
(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"]; Supervision --> Bernhard; Supervision --> Mathias; Supervision --> Tobias; Supervision --> TobiasF; Supervision --> All; Supervision --> Bernhard_Tobi; class Tobias tobi; class Mathias mathias; class Bernhard bernhard; class TobiasF tobiasF; class All all; class Bernhard_Tobi bernhard_tobi;
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; (iii) what you are interested in (bachelor/master and project/thesis).
-
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
We expect you to implement a tool in JavaScript as demonstration tool for our lectures. JavaScript makes it possible for us to host the tool on our webpage, ensure that future students will also be able to use it. See the list.