Sound basic knowledge in mathematical logic, discrete mathematics, automata and computability theory as taught in the modules "Discrete Structures" and "Theoretical Computer Science I + II". In addition, programming skills as acquired in the "Programming Course".
Justification:
The methods presented in the lecture are based on an operationalization of semantics by reduction to logical encodings and mechanized testing of logical statements. An understanding of these contents as well as their tool-technical implementation requires the basics from the aforementioned courses.

• 1st deadline: Submission of the semester project incl. one week after the end of the lecture period of the lecture period; followed by a colloquium and a final discussion
• 2nd deadline: Repeat of the submission of the semester project incl. written elaboration two weeks before the beginning of the following semester followed by colloquium and final discussion

Semester project

The module provides an overview over semantic models for reactive systems, real-time systems ,and hybrid systems, as well as examples of corresponding specification logics. It explains state-exploratory verification procedures in both explicit and symbolic variants. The knowledge acquired can be employed in all domains requiring the development of reliable software and hardware systems is concerned
Professional competences
The students:

• make a sound judgement on the scope of the certificates that can be obtained with formal methods
• assess the suitability of available verification tools for a particular problem and system class
• use automatic analysis tools on real systems, interpret the results obtained and subsequently improve the system under investigation in an informed and targeted manner
• prepare system models for automatic analysis procedures and encode them symbolically (or otherwise)
• design and implement their own verification algorithms

Methological competences

The students:

• master the mathematical modelling of complex and heterogeneous dynamical systems
• know relevant mathematical models of dynamic systems and can instantiate them to new problem classes

Social competences
The students:

• together in a team develop and implement basic algorithms of automatic verification
• discuss the advantages and disadvantages of algorithmic alternatives and different formalisations

Self competences

The Students:

• can assess their technical and methodological understanding
• reflect on their problem-solving competence with reference to the procedures and methods presented