10.90.136.11: Created page with "= Logic in Computer Science = * '''Course name:''' Logic in Computer Science * '''Course number:''' XYZ * '''Knowledge area:''' Math, C..."

2021-07-30T10:39:31Z

Created page with "= Logic in Computer Science = * '''Course name:''' Logic in Computer Science * '''Course number:''' XYZ * '''Knowledge area:''' Math, C..."

New page

= 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 ==

<div style="color: blue">

* 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.

</div>
== 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 ==

<div style="color: blue">

* Homeworks (60%)
* Final Exam (40%)

</div>

BSc:LogicInComputerScience - Revision history

10.90.136.11: Created page with "= Logic in Computer Science = * '''Course name:''' Logic in Computer Science * '''Course number:''' XYZ * '''Knowledge area:''' Math, C..."