BSc:LogicInComputerScience

From IU
Jump to navigation Jump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

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%)