|
Instructors: Prof. Ph.D. Sebastian Faust
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:
- | -
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.
Further Grading Information:
Link to Moodle https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1199
|
