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.