Decision Procedures for Verification
Viorica Sofronie-Stokkermans <email@example.com>
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).
One of the most important research objectives in mathematics and
computer science is to obtain means of reasoning in and about
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.
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
- A. Bradley and Z. Manna:
The Calculus of Computation. Decision Procedures with Applications to Verification.
- Daniel Kroening and Ofer Strichman:
An Algorithmic Point of View