Here are some ideas. Some of them have been already given, but feel free to find some inspiration.

Most of the thesis and projects I supervise are not Isabelle related and go through our group’s flow. Therefore, unless you are mostly interested in Isabelle topics, you should follow the process described there.

If you are interested in one project (or in something related), please write me an email (following the guidelines!).

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 me an email.

SAT Encoding

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

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

While the two projects below do not require to write proofs, you will still spend a lot of time looking at them. So you will have to think about bound variables in the current context and free variables (leading to failed reconstruction).

Improved parsing for veriT proofs in Isabelle

• Prerequisit: no knowledge of Isabelle nor SMT solvers nor Standard ML is required, but knowledge of a functional language and some understanding of proofs is required.
• Theme: The proof assistant Isabelle relies on external tools to prove goals. However, it does not trust those tools and checks the proof that the external tools generate. For this project, we are interesting in the SMT solver veriT. Currently the whole proof returned by veriT is entirely parsed before being checked. This work intends to parse the proof steps before we need them in order to improve performance.
• Outcome: The resulting code should be added to the Isabelle repository.

Updating Z3 in Isabelle

• Prerequisit: no knowledge of Isabelle nor SMT solvers nor Standard ML is required, but knowledge of a functional language and some understanding of proofs is required.
• Theme: The proof assistant Isabelle relies on external tools to prove goals. However, it does not trust those tools and checks the proof that the external tools generate. For this project, we are interesting in the SMT solver Z3. Isabelle relies on a very old version of Z3 and it is known that the latest version does not work with Isabelle due to bugs in the proof output Z3. The aim of this project is to find if we can update Z3 to a newer version. This will require both to fix the proof reconstruction (because some new features were added to the proof output) and check if the generated proofs are correct.
• Outcome: The resulting code should be added to the Isabelle repository.

Testing Infrastructure for IEE754 floats in Isabelle

• Prerequisit: some knowledge of Isabelle is required, but a strong knowledge is definitively a plus (in order to also fix discovered issues)
• Theme: The proof assistant Isabelle does not yet have bindings to generate floating points, but Peter Lammich is working on it. However, it is not clear if the generated code has the same behaviour. The aim of this project is to create a test-suite to check that the behaviour is the same (especially for edge cases involving NaN, infinity, …).
• Warning: this project would be partly co-advised with Peter Lammich. It is also at the edge between developing Isabelle and using 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

• Prerequisit: strong knowledge of Isabelle is required (see my lecture for SS-22). Knowledge of the Refinement Framework is a plus (but it is not too hard to learn). No knowledge of SAT solving is needed
• Theme: IsaSAT currently uses only one decision heuristic, namely variable move to front. The aim for this project is to add a second one targeting satisfiable instances.
• Outcome: The resulting code should be added to IsaSAT.
• Warning: this is a challenging project because it is using Isabelle and the Refinement Framework, but it does not require advanced concepts.

Incremental Reconstruction Stack

• Prerequisit: strong knowledge of Isabelle is required (see my lecture for SS-22). No knowledge of SAT solving is needed.
• Theme: SAT solver simplify the formula they are currently solving in ways that are not equisatsifiable, i.e., a model of the resulting formula must be fixed to be a model of the original formula. The aim of this project is to formalize this process for an incremental SAT solver. This builds on the incremental reconstruction stack for non-incremental stacks
• Outcome: The resulting code should be added to the IsaFoL repository.
• Warning: This project is too large for a bachelor project/thesis.

Unsorted

• OTFS in the CDCL rewrite system
• Model reconstruction for autarkies
• Autarky detection

Isabelle Refinement

Unsorted

• Memory module for sharing of lists for Pastèque

Isabelle Abstracting

Use Corrode to verify a Rust DPLL solver or something else.

So far there have been two approaches:

• DPLL solvers have been verified only via synthesis, so starting from the Isabelle extracting it to code. IsaSAT does it with CDCL solving instead of DPLL.
• Automatic verification with SMT solvers like CreuSAT where only the “unsat” answer is verified (the idea being that you verify that the derivation of false is verified).

The aim of this project is to try the latter approach in Isabelle. More concretely, you would implement a (at-first very simple) DPLL SAT solver which you would connect to the existing DPLL solver.

Isabelle LLVM

Unsorted

• Mini-GMP for Isabelle LLVM binding.

Teaching Related

Example of done topic

Encoding the Rummikub for SAT

See the Rummikub game here. Partially given.

Reconstruction Stack

• Prerequisit: strong knowledge of Isabelle is required (see my lecture for SS-22). No knowledge of SAT solving is needed.
• Theme: SAT solver simplify the formula they are currently solving in ways that are not equisatsifiable, i.e., a model of the resulting formula must be fixed to be a model of the original formula. The aim of this project is to formalize this process.
• Outcome: The resulting code should be added to the IsaFoL repository.
• Warning: This project is most likely too large for a bachelor project/thesis.