Presented by: Gerald Futschek, Gernot Salzer
Elective course (Wahllehrveranstaltung) in the master studies "Computational Intelligence" (066931), "Software Engineering & Internet Computing" (066937) and "Technische Informatik" (066938), and in the international master program "Computational Logic (Erasmus-Mundus)" (066011).
The default language is German. However, if someone in the audience is not sufficiently fluent in German the course will be given in English.
Written exam: June 21, 2010, 15:30-17:00, FH 3
Slides: April 26, 2010
Lab assignments 2010:
The deadline for the last assignment was on June 13, 2010. There is an extended, firm
deadline for late submissions or improved versions on June 20, 2010.
You should have received an email acknowledging the receipt of your submission
and containing a list of possible dates for the final, individual meeting.
If you did not receive the email, contact
salzer@logic.at.
Course dates 2010: every Monday, 15:30-17:30,
FH 3
First meeting: March 8, 2010
The aim of the course is to train the theoretical and practical skills required for the formal verification of computer programs.
The course presents the logical foundations of formal verification (Hoare logic, dynamic logic), the development of correct programs using assertions, pre/post-conditions and invariants, and discusses the verification of sequential, parallel and distributed programs. Selected verification systems are used for the practical exercises.
The course consists of a lecture and practical exercises.
In summer term 2010, the lecture takes place every Monday, 15:30-17:30,
FH 3
First meeting: March 8, 2010.
The practical exercises consist of several assignments to be solved at home and individual meetings for discussing the solutions. We use the tool Perfect Developer by the company Escher Technologies; for more information see www.logic.at/perfect.
Slides: March 22, 2010
Gernot Salzer