Sarek

4 ms·

1. 1.▲
   by Sarek 4y ago

   This was asked in the Rust Zulip as well, and is actually the original idea which this thesis evolved from (Xavier said something along the lines of "My supervisor and I have talked about how cool it would be to have a solver which ver
2. 2.▲
   by Sarek 4y ago

   Ah, I knew I forgot something! Thanks, I licensed it under the MIT license now:)
3. 3.▲
   by Sarek 4y ago

   It does assume enough RAM, as it has no way of knowing how much RAM the target machine will have. It is thus correct with regards to the model specified by Rust, but a program which is proven correct in Creusot may get an OOM-error. A note
4. 4.▲
   by Sarek 4y ago

   Generating a proof and checking it is definitely a step up, but it does have a few issues. - SAT is in NP, and UNSAT is in CoNP. This means that proofs take a lot of space to store and a lot of time to check. Proofs are usually run with 5x