# Course Identification

Mathematics module: The Mathematics of Programming
20216202

## Lecturers and Teaching Assistants

Prof. Mordechai Ben-Ari
N/A

## Course Schedule and Location

2021
Second Semester
Tuesday, 11:15 - 13:00
02/03/2021
31/08/2021

## Field of Study, Course Type and Credit Points

Science Teaching (non thesis MSc Track): Lecture; Obligatory; Regular; 3.00 points

לתלמידי שני השנתונים

No

## Restrictions

20
For students in the Rothschild-Weizmann program only

Hebrew

## Attendance and participation

Obligatory

Numerical (out of 100)

30%
70%
The exam will be given at 14.7 and the students will have 36 hours.

Take-home exam

N/A
N/A
-
N/A

3

## Syllabus

Logic is the mathematical foundation of computer programming. We will explore two topics:

1. SAT solving: A problem is encoded as a formula in propositional logic and the SAT solver software searches for a satisfying interpretation, from which a solution to the problem is obtained.

2. Logic is used to verify the correctness of a computer program, especially a concurrent program.

Topics:

1. Propositional logic: syntax, interpretations, semantic tableaux, soundness and completeness, clausal form, resolution, DPLL algorithm for SAT solving, solving problems using a SAT solver.
2. The formal model of a concurrent program. The mutual exclusion problem. Semaphores.
3. Temporal logic.
4. Model checking for verifying concurrent programs.

## Learning Outcomes

Upon successful completion of the course- students should be able to:

1. Explain the theory of propositional logic and construct semantic tablueux for formulas.
2. Describe the DPLL algorithm for SAT solving.
3. Use a SAT solver to encode and solve problems.
4. Explain the syntax and semantics of temporal logic.
5. Use a model checker to verify a concurrent program.

Lecture notes will be posted and are required reading.

LearnSAT tutorial is available on the software's website.

M. Ben-Ari. Mathematical Logic for Computer Science (Third Edition). Springer, 2012.

Software

1. LearnSAT SAT solver: https://github.com/motib/LearnSAT
2. Erigone model checker: https://github.com/motib/erigone

N/A