City: Saint Petersburg Novosibirsk Kazan Language: Русский English

Software Verification
Saint Petersburg / spring 2008, посмотреть все семестры

Enroll in the course to get notifications and to be able to submit home assignments.
Register to enroll now Login

The course introduces the theory and practice of formal methods for the design and analysis of software systems. The course will cover the underlying logical and theoretical concepts, with focus on the algorithmic solutions, and heuristics to cope with the high computational complexity. Lectures:

  • Introduction to model checking: system modeling and logic specifications
  • Abstraction in model checking: Predicate abstraction; CEGAR-based software model checking
  • SAT-based software model checking
Date and time Class|Name Venue|short Materials
01 May
14:50–16:20
Assuring software quality by model checking, Lecture ПОМИ РАН slides,  video
01 May
16:20–17:50
State-event-based reasoning and deadlock detection, Lecture ПОМИ РАН slides,  video
02 May
14:50–16:30
Automated verification of security policies in mobile code, Lecture ПОМИ РАН slides,  video
02 May
16:30–18:00
Deadlock detection, Lecture ПОМИ РАН slides