An important issue in the development of large software systems is the specification of their desired structural and dynamic properties. To avoid the impreciseness and ambiguities of specifications in natural language, a number of specialized formal languages, based on logic and mathematics, have been developed. Moreover, these languages are supported by algorithms and tools allowing various types of analysis and verification.
The course covers the following main topics:
* Formal verification
* Labelled transition systems as models of systems
* Linear temporal logic
* Computation tree logic
* Symbolic model checking
* Model checking probabilistic systems