Robert Brummayer,
"C32SAT - Ein Erfüllbarkeits-Überprüfer für Ausdrücke in C"
, 2-2006
Original Titel:
C32SAT - Ein Erfüllbarkeits-Überprüfer für Ausdrücke in C
Sprache des Titels:
Deutsch
Original Kurzfassung:
Aufgrund der steigenden Software Komplexität wird formale Verifikation immer bedeutender. In dieser Diplomarbeit wird die Verwendung einer Software, die „C32SAT“ genannt wird, vorgeschlagen. Es wird die Implementierung und die zugrundeliegenden Konzepte dieser Software vorgestellt. Die Frage welche diese Diplomarbeit beantwortet, ist, ob C32SATs funktionale Repräsentation von booleschen Ausdrücken in C verwendet werden kann, um Erfüllbarkeit effizient zu überprüfen, oder nicht.
Zuerst wird eine Motivation für formale Verifikation gegeben. Dann wird das Erfüllbarkeitsproblem der Aussagenlogik, And-Inverter Graphen, Zwei Level Optimierung und Transformationen in konjunktive Normalform vorgestellt. Danach wird C32SAT, die Eingabesprache, Semantik, Operatoren, Design Entscheidungen, Architektur, Algorithmen, verwandte Arbeiten und Benchmarks vorgestellt.
Sprache der Kurzfassung:
Deutsch
Englischer Titel:
C32SAT – A Satisfiability Checker for C Expressions
Englische Kurzfassung:
Formal verification becomes more and more important as software complexity increases. In this thesis we propose the use of a formal verification tool called „C32SAT“. We discuss its implementation and underlying concepts. The questions which this thesis addresses is wheter C32SATs functional representation of boolean C expressions can be used to check satisfiability efficiently or not.
First we give a motivation for formal verification. Then we discuss the satisfiability problem of propositional logic, And-Inverter Graphs, two level optimisation and transformations into conjunctive normal form. Afterwards we discuss C32SAT, its input language, semantics, operators, design decisions, architecture, algorithms, related work and benchmarks.