Chair of Computer Architecture

University of Freiburg

Here are some ideas. Some of them have been already given, but feel free to find some inspiration. If you are interested in one project (or in something related), please write me an email (following the guidelines!).

The Chair also has an internal list. If you are interested in what we are doing, write Armin Biere an email.

I consider bachelor and master thesis/projects to be community work, so if you have a fun idea that matches my interests, feel free to drop an email.

SAT Encoding

Encoding the Rummikub for SAT

See the Rummikub game here

Mastermind encoding

Or “are you the one” solver (yes, the TV reality show) for sharp-SAT to count how many solutions are still possible.


Isabelle is a proof assistant, but not all subjects require any knowledge of it.

Remark that for master projects and master thesis, it is also possible to learn Isabelle as part of the project – however learning Isabelle and Sepref for the code synthesis is too much.

Isabelle Development

Improved parsing for veriT proofs in Isabelle

Updating Z3 in Isabelle

Testing Infrastructure for IEE754 floats in Isabelle

IsaSAT improvement (Isabelle usage)

I have several ideas. Two of them are written below. If you have more ideas or want to do something different, feel free to write me.

Implementing ACIDS/VSIDS for IsaSAT

Reconstruction Stack


Isabelle Refinement


Isabelle LLVM