Verified SAT-based Decision Procedures

Topic no longer available

Supervisor Tobias Philipp
Start

The satisfiability problem (SAT) is one of the most prominent problems in theoretical computer science and has many applications in software verification, planning, bioinformatics or scheduling. Satisfiability solvers have become more complex in recent years due to inprocessing techniques and parallel computing. This raises the question whether the results of these solvers can be trusted. To gain confidence in the correctness of the results, SAT solvers can emit unsatisfiability proofs that can be validated using a checker.

However, the translation from SAT-based decision procedures, such as in answer set programming, bounded model checking, etc. can also be incorrect. Therefore, implementing such translations to SAT in a functional programming language, and afterwards proving correctness of the the translation is important. The combination of mechanically verified translations with the certificates from SAT solvers then leads to trustful computations.