# Decision Procedures for Verification

Instructor:

Viorica Sofronie-Stokkermans <sofronie@uni-koblenz.de>

### Exam

### Contents

The goal of this lecture is to present the recent results
in automated reasoning, especially decision procedures,
and their applications in verification (e.g. in program verification).

#### Motivation

One of the most important research objectives in mathematics and
computer science is to obtain means of reasoning in and about
complex systems.
Proving properties of such systems is extremely important.
In safety-critical systems even small mistakes can provoke disasters.
Since the amount of data which has to be handled in all the application
domains mentioned above is usually huge, computer support is necessary.
General-purpose programs for solving all types of problems mentioned
above do not exist. However, for concrete application domains automatic
procedures exist. The goal of this lecture is to present specific
domains in verification
for which efficient methods for automated reasoning exist.

### Recommended literature

#### Course material from other lectures

#### Propositional logic, first-order logic

- Melvin Fitting:

*First-Order Logic and Automated Theorem Proving.*

Springer-Verlag, New York, 1996.
- Uwe SchÃ¶g:

*Logik für Informatiker.*

Spektrum Akademischer Verlag, 2000

#### Decision procedures

- A. Bradley and Z. Manna:

*The Calculus of Computation. Decision Procedures with Applications to Verification. *

Springer 2007.

- Daniel Kroening and Ofer Strichman:

* Decision Procedures
An Algorithmic Point of View *

Springer 2008.