Course Identification

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.

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