Logic in Computer Science

Course name: Logic in Computer Science
Course number: XYZ
Knowledge area: Math, Computational Science

Administrative details

Faculty: Computer Science and Engineering
Year of instruction: 1st year of BS
Semester of instruction: 1st semester
No. of Credits: 4 ECTS
Total workload on average: 144 hours overall
Frontal lecture hours: 2 per week
Frontal tutorial hours: 2 per week
Lab hours: 0 per week
Individual lab hours: 2
Frequency: weekly throughout the semester
Grading mode: letters: A, B, C, D

Prerequisites

None

Course outline

In recent years, powerful tools for verifying software and hardware systems have been developed. These tools rely in a crucial way in logical techniques. Propositional and predicate logic are presented in detail, as well as some specialized logics (temporal logics) used for reasoning about the correctness of computer systems. A sound basic knowledge in logic is a welcome prerequisite for courses in program verification, formal methods and artificial intelligence. The course presents: propositional, predicate and temporal logics, as well as software verification techniques such as Hoare-style axiomatic semantics, model-checking and testing.

Expected learning outcomes

After taking the course, students will be able to

explain the notion of model of a first-order language and the meaning of the completeness and soundness theorems
describe the principles behind fundamental software verification techniques.
apply the principles to the construction of verification tools, in particular program provers.
judge the relevance of logical reasoning in computer science
analyse the applicability of logical tools to solve problems in computer science, i.e. finding bugs with the use of model checking

Expected acquired core competences

write and check proofs in natural deduction for propositional and predicate calculus
specify properties of a reactive system using logic .
apply different techniques and tools for program proving.

Textbook

Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems, second edition. Cambridge University Press, 2004.
Aaron Bradley and Zohar Manna. The Calculus of Computation. Springer, 2007.
Bertrand Meyer. Introduction to the Theory of Programming Languages. Prentice Hall, 1990.
Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 2000.
Mauro Pezzè, Michal Young: Software Testing and Analysis: Process, Principles and Techniques, Wiley, 2007.

Reference material

Lecturing and lab slides and material will be provided.

Required computer resources

Students should have laptops. Different tools will be installed during the course.

Evaluation

Homeworks (60%)
Final Exam (40%)

BSc:LogicInComputerScience

Contents