Decision Procedures for Verification

Instructors:
  • Viorica Sofronie-Stokkermans <sofronie@uni-koblenz.de>
  • Exercises: Markus Bender
  • For questions: e-mail to sofronie@uni-koblenz.de
    • Time and place:
  • Lecture: Mondays, 14:00-16:00, Room C 206
  • Exercise: Mondays, 16:00-18:00, Room B 017
  • Slides
  • Exercise Sheets

    • Exam
  • Exam: Termin 1 Friday, 22.02.2013, starts: 10:00 (oral examination); Room B 225
  • Question and answer sessions: 19.02.2013, 11:00, Room B 225 and 21.02.2013, 11:00, Room B 225.

  • List of topics: [summary.pdf]
  • New: Collection of exercises [collection-exercises-16-02.pdf]

  • Exam: Termin 2 Friday, 21.03.2013, starts: 11:00 (oral examination); Room B 225
  • Question and answer session: 18.03.2013, 11:00, Room B 225.

    • 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.