SAT & SMT

June 8, 2022 at 8:51 pm

Basic Concepts

Proof Checker

Solver

Verified/Certified Solver

VeriT

  • Can be used with external checkers, e.g. SMTCoq

versat: A Verified Modern SAT Solver

  • No code, not usable
  • Dependent Type; Guru-lang

Papers

SMT Solver Funzzing

Formal(ly Verified) SAT/SMT Solver

Proof Checking

Also see the related articles.

Other Resources

SystemPapers

September 12, 2021 at 8:54 pm

By topic

FaaS Papers, mainly in TEE

Generated List of Papers:

Apache Flink™: Stream and Batch Processing in a Single Engine

April 29, 2022 at 1:00 pm

ObliDC: An SGX-based Oblivious Distributed Computing Framework with Formal Proof

April 29, 2022 at 12:58 pm

Proof-carring Code

January 19, 2022 at 8:13 pm