Logik und Verifikation

von Prof. Dr. rer. nat. Jürgen Dix



This course is about logic based formal methods and how to use them for verification in computer science.
It rigorously defines the language and semantics of sentential logic (SL) and first-order logic (FOL).
We introduce the notion of a model, and show how hardware and software systems can be modelled within this framework. We also consider
semantic entailment vs. syntactic derivability of formulae and how these two notions are related through correctness and completeness. Completeness is formally proved for SL and extensively discussed for FOL (in the form of refutation completeness).
Both logics are applied to important verification problems: SL and its extension LTL for verifying linear temporal properties in concurrent systems, and
FOL for verifying input/output properties of programs (the Hoare calculus).
We show how the resolution calculus for FOL leads to PROLOG, a programming language based on FOL.
We also show that SL leads to a declarative version of PROLOG: Answer Set Programming (ASP), that can be used to solve problems expressible on the second level of the polynomial hierarchy.
While ASP is not a full-fledged programming language, it can be used for many naturally ocurring problems and it allows to model them in a purely declarative way.

1. Introduction
2. Sentential Logic (SL)
3. Verification I: Reactive Systems
4. First-Order Logic (FOL)
5. Verification II: Hoare Calculus
6. From FOL to PROLOG