From b36aacd53874c49e77493ac6ecceabf0b1968154 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Sarek=20H=C3=B8verstad=20Skot=C3=A5m?= Date: Thu, 11 Apr 2024 01:27:25 +0200 Subject: [PATCH] Update README --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 8d30ddf7..7270ad1e 100644 --- a/README.md +++ b/README.md @@ -83,6 +83,7 @@ There are a bunch of tests in the [Creusot repository](https://github.com/xldeni You could also check out [Friday](/Friday/) and [Robinson](/Robinson/) for a couple of verified solvers which are both easier to grok algorithmically and proof-wise. +Oh, and yeah, read the [thesis](/SarekSkot%C3%A5m_thesis.pdf/). You don't have to read the whole thing, but it has a pretty good introduction to Creusot, program verification, and SAT solving. At least I think it is pretty good, and I've also gotten feedback from people not all that familiar with these kinds of things that it is fairly accessible. ## Overview of the repository