|
HU Credits:
2
Degree/Cycle:
2nd degree (Master)
Responsible Department:
Computer Sciences
Semester:
1st Semester
Teaching Languages:
English and Hebrew
Campus:
E. Safra
Course/Module Coordinator:
Guy Katz
Coordinator Office Hours:
By appointment
Teaching Staff:
Dr. Katz Guy
Course/Module description:
Ensuring the correctness of software is both difficult and important. While the problem is undecidable in general, there is a wide range of algorithms and techniques for solving it in many practical cases. In this course we will learn how the correctness of software can be mathematically proven using automated tools called solvers. We will explore some of the algorithms these tools rely on, and also gain hands-on experience in using them.
We will focus on: Boolean satisfiability (SAT) solvers, Satisfiability Modulo Theories (SMT) solvers, and Linear Programming (LP) solvers
And their applications in analyzing software through deductive reasoning, symbolic execution, and model checking. We will also learn about applying these techniques, both theoretically and practically, to ensure the correctness of software generated through machine learning.
Course/Module aims:
To expose the students to the challenges, algorithms, methods and state-of-the-art tools for software analysis, and present some of the open problems in the field
Learning outcomes - On successful completion of this module, students should be able to:
Understand the core theory behind automated solvers, apply these tools to check the correctness of various kinds of software, and participate in research in the field
Attendance requirements(%):
Attendance is required
Teaching arrangement and method of instruction:
Synchronous online lectures
Course/Module Content:
SAT solvers, SMT solvers, LP solvers, deductive reasoning, symbolic execution, model checking, verification of neural networks
Required Reading:
-
Additional Reading Material:
Grading Scheme :
Additional information:
The course may be given in English
|
close