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“) |
Tobias Philipp (talk | contribs) No edit summary |
||
| 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 | |||
|Forschungsgruppe=Wissensverarbeitung | |||
|Abschlussarbeitsstatus=Offen | |||
|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. | |||
}} | |||
Revision as of 16:13, 12 October 2015
Verifizierte SAT-basierte Entscheidungsprozeduren
Verfügbar als Thema einer Bachelorarbeit, Masterarbeit, Diplomarbeit, Studienarbeit
- Betreuer Tobias Philipp
- Wissensverarbeitung
- 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.
