The course has three parts: propositional logic, predicate logic and temporal logic. Each part is divided into basics on logic and applications to software engineering. In the part on predicate logic, we use Alloy.