Topic Verified SAT based Decision Procedures/en: Difference between revisions
From International Center for Computational Logic
Tobias Philipp (talk | contribs) (Die Seite wurde neu angelegt: „x“) |
Markus Krötzsch (talk | contribs) No edit summary |
||
| (One intermediate revision by one other user not shown) | |||
| Line 1: | Line 1: | ||
{{Abschlussarbeit | |||
|Titel DE=Verifizierte SAT-basierte Entscheidungsprozeduren | |||
|Titel EN=Verified SAT-based Decision Procedures | |||
|Abschlussarbeitstyp=Bachelor, Master, Diplom, Studienarbeit | |||
|Betreuer=Tobias Philipp | |||
|Abschlussarbeitsstatus=Nicht mehr verfügbar | |||
|Beschreibung EN=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. | |||
}} | |||
Latest revision as of 21:56, 16 April 2021
Verifizierte SAT-basierte Entscheidungsprozeduren
Thema nicht mehr verfügbar
- Betreuer Tobias Philipp
- Beginn
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.
