Courses

Software Verification (10146)

Abstract:

This module teaches the theory and practice of formally proving the correctness of imperative sequential programs using the Dafny formal verification language and tool set.

Software Systems Modeling (10148)

Abstract:

The module consists of two parts. In the first part we will study simple reactive systems and learn how to model them as transition systems and how to express properties using temporal logic formulas. We will then learn how to use a model checker to check if the models satisfy the properties. In the second part we will learn how to describe information systems using relational logic and how to express business rules and structural invariants using relational logic formulas. Finally, we will learn how to use the Alloy analyzer to check that the model satisfies the business rules and structural invariants.

Ethics in Software Engineering (10827)

Abstract:

Introduction to the basic ideas in the philosophy of morality and ethics Challenges that life in the high-tech industry poses

The knowledge-rich industry exposes its workers to numerous moral challenges and ethical dilemmas:

Is it legitimate to work in a company without ethical principles?

What about companies that vehemently oppose Israel?

Is it ethical to work in a company involved in gambling?

And what would Aristotle and Kant say about all of this?

In each lesson, dilemmas from everyday life in the industry will be presented in studies and in general. Some of the examples are difficult to hear and contain triggers for prejudice, chauvinism, profiteering from murder, and more.