Decision Procedures for Verification

Instructor:
  • Viorica Sofronie-Stokkermans <sofronie@uni-koblenz.de>
  • For questions: e-mail to sofronie@uni-koblenz.de
    • Time and place:
  • Exercise: Tue, 14:00s.t.-16:00, Room K 107
  • Lecture: Thu, 12:00s.t.-14:00, Room E 427
    • We try to find a new time for the lecture and for the exercises.
    We created a doodle for this. Please fill in the dates which are
    possible for you until Thursday, 24.10.2013, 17:00.

    Doodle: Umfrage zur Vorlesung/Übung

  • Slides
  • Exercise Sheets

    • News
  • The times for exercise and lecture are now switched.
    The date and time of the lecture and exercises are:
  • Exercises: Tue. 14:00 s.t-16:00,
  • Lecture: Thu. 12:00 s.t.-14:00.
  • The date and time of the lecture and exercises changed as follows:
  • Lecture: Tue. 14:00-16:00,
  • Exercises: Thu. 12:30-14:00.
  • Exception:
  • Tuesday, 29.10.2013, 14:00-16:00: exercise (M. Bender)
  • Thursday, 31.10.2013, 12:30-14:00: lecture

    • Exam
  • Termin 1. Written exam: Tue. 25.02.2014, duration: 2h, starting time: 11:00 s.t.; Room: B 017

  • Summary of topics: [summary.pdf]
  • Question/Answer Session:
    • Friday, 21.02.2014, 14:00, Room B 225
    • If you cannot take part on Friday, 21.02 but have questions and
      would like to meet on Monday 24.02 please send me an e-mail.
  • Klausureinsicht: 13.03.2014, 11:00, B 225

  • Termin 2: There will be a second possibility to take the exam towards the end of the lecture-free part of the semester.
    The precise date, time and place will be announced.

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