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:
- Propositional logic: syntax, interpretations, semantic tableaux, soundness and completeness, clausal form, resolution, DPLL algorithm for SAT solving, solving problems using a SAT solver.
- The formal model of a concurrent program. The mutual exclusion problem. Semaphores.
- Temporal logic.
- Model checking for verifying concurrent programs.