We shall introduce the main technologies employed in automated reasoning, based both on saturation and on backtracking methods. Applications covering computational algebra topics as well as formal verification problems will be considered. The student will be introduced to some state-of-the-art tools, like SAT- and SMT-solvers, superposition provers, finite and infinite state model checkers.
Expected learning outcomes
To be acquainted with automated reasoning tools (SMT-solvers and superposition provers), from the point of view both of practical use and of theoretical foundations.
Lesson period: Second semester
(In case of multiple editions, please check the period, as it may vary)