This course gives an introduction to computational logic, i.e., to those aspects of logic that can be supported by software or are relevant for software development: satisfiability solving in propositional logic, computer-supported and fully automated proving in first-order logic, and decision procedures for certain (combinations of) logical theories.

This exercises lecture is an extension of the main course on Algorithms and Data Structures. It will provide the opportunity for putting into practice all the subjects discussed during the course, both by implementing, analysing, optimizing the presented algorithms, and by exploring additional use cases and new algorithms. It is addressed both to students who started programming only last year (beginners), and to students with advanced skills.

This course gives a survey on the use of formal methods for the development of reliable software using freely available tools.

This seminar discusses techniques and tools for formal methods and/or automated reasoning such as formal specification languages, program verification systems, model checkers, interactive proof assistants, automated theorem provers, satisfiability solvers, decision procedures, etc.