CASUS Seminar on Numerical Techniques and Algorithms, Gyula Sallai, SonarSource S.A.

As embedded systems are becoming more and more common in our lives, the importance of their safe and fault-free operation is becoming even more critical. Model checking can prove both the presence and absence of certain errors in software systems, making it suitable for verifying safety-critical systems. This field has made a tremendous progress in the last decades, providing a great set of fast and effective algorithms. In this talk, we are going to walk through some of the most wellknown model checking algorithms and some of the problems one can face when implementing a model checking tool.