Correctness is a major concern in embedded systems. Model checking can fully automatically prove formal properties about digital hardware or software. Such properties are given in temporal logic, e.g., to prove "No two orthogonal traffic lights will ever be green at the same time."
But what are the limitations of model checking? How are the models generated from a given design? And how do the underlying reasoning algorithms work so effectively in practice despite a computational complexity of NP hardness and beyond?
The lecture will answer these questions. Open source tools will be used to gather a practical experience.
Further information is available in stud.ip (use link above).
