Decision Procedures for Verification

Instructor:
  • Viorica Sofronie-Stokkermans <sofronie@uni-koblenz.de>
  • For questions: e-mail to sofronie@uni-koblenz.de

  • You can also ask questions in the Forum.
    • Time and place:
  • Lecture: Mo, 10:00 c.t.-12:00, E 524 New: B 227
  • Exercise: Thu, 12:00-14:00, A 120 New: B 227

  • Slides
  • Exercise Sheets

  • OLAT Course
  • Forum: under OLAT

  • Audio-commented slides are available in Panopto

    • News

     (latest news first)
  • 5.02.2024: OLAT seems to be offline. If you have questions and cannot attend the lecture in presence please send the questions to me per e-mail or use the Forum as soon as OLAT functions again.
  • 15.12.2023: The lecture and exercises will take place in hybrid mode from now on:
    -- Room change: Both exercise and lecture take place in Room B 227 & BBB
  • Exercise on 27.11.23
  • Lectures on 20.11.23 and 23.11.23
  • Lectures on 30.10.23 and 2.11.2023
  • The first exercise session will take place on 9.11.2023
  • The first exercise sheet will be available on 2.11.2023

    • Exam:

    Contents

    The goal of this lecture is to present the recent results in automated reasoning, especially decision procedures, and their applications in 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 computer science (with an emphasis on verification) for which efficient methods for automated reasoning exist.