C32SAT - Ein Erfüllbarkeits-Überprüfer für Ausdrücke in C

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.