|
Instructors: Dr. rer. nat. Richard Bubel
Event type:
Integrated Course
Org-unit: Dept. 20 - Computer Science
Displayed in timetable as:
FormMeth SWdesign
Subject:
Crediting for:
Hours per week:
3
Language of instruction:
German
Min. | Max. participants:
- | -
Digital Teaching:
The course is given in person. The course website is:
https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1558
Course Contents:
- Modelling of concurrent software with the ProMeLa language
- Formalisation of safety and liveness properties in propositional temporal logic
- Theoretical Foundations of Model Checking
- Verification of ProMeLa programs using the model checker SPIN
- Syntax, semantics, and sequent calculus for typed first-order logic
- Foundations of the contract-based software specification language JML
- Dynamic logic as a first-order program logic
- Formal software verification by symbolic execution and invariant reasoning
- Tool-based verification of Java programs with the verification system KeY
Literature:
First part of lecture:
- Ben-Ari: Principles of the SPIN Model Checker, Springer
- Holzmann: The SPIN Model Checker, Addison-Wesley
Second part of lecture:
- Beckert et al.: Verification of Object-Oriented Software, Springer
Literature recommendations will be updated regularly.
Preconditions:
Recommended:
Programming with Java and familiarity with propositional logic is expected.
Participation of lecture “Aussagen- und Prädikatenlogik”.
Fundamental mathematical knowledge.
Online Offerings:
The course website (announcements, teaching material etc.) is available at
https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1558
|
