Advanced Computer Science: Multi-Core Computing [MSc]

Automated Reasoning and Verification


Unit code: COMP60332
Credit Rating: 15
Unit level: Level 6
Teaching period(s): Semester 2
Offered by School of Computer Science
Available as a free choice unit?: Y

Requisites

None

Aims

The course aims at providing an understanding of propositional reasoning and first-order reasoning, giving an introduction to theoretical concepts and results that form the basis of current automated reasoning systems based on DPLL and resolution, and discussing verification as an important application domain.

Overview

Automated reasoning has a wide range of applications fromproving mathematical theorems automatically to verification of hardware and software. For example, major software and hardware industries such as Microsoft and Intel intensively use automated reasoning methods in verification of their products.
This course introduces automated reasoning methods for propositional and first-order logic. The course develops theoretical foundations of automated reasoning with focus on efficiency and applications.

Teaching and learning methods

Lectures

Lecturers will be interspersed with example classes and labs on teaching days

Examples classes

Example classes will take place on teaching days

Laboratories

Labs will take place on teaching days

Learning outcomes

Learning outcomes are detailed on the COMP60332 course unit syllabus page on the School of Computer Science's website for current students.

Employability skills

  • Analytical skills
  • Problem solving
  • Research
  • Written communication

Assessment methods

  • Written exam - 50%
  • Written assignment (inc essay) - 50%

Syllabus

The following lists the topics to be covered in the course. The teaching days will contain a mixture of lectures, examples classes, supervised laboratories and self-study. The number of lectures for each topic are given in brackets.

      * Introduction (1)

      * Orderings, multi-sets (1)

      * Propositional reasoning

           Language of propositional logic, semantics, truth tables (1)

           Satisfiability, validity, equivalence, decidability (1)

           Normal forms, CNF, clauses, optimised normalisation (1)

           Propositional resolution (1)

           DPLL and SAT-solving with backjumping, lemma learning (2)

           Logical modelling (1)

      * General first-order reasoning

           Language of first-order logic, semantics (2)

           Normal forms, clauses (1)

           Herbrand interpretations (1)

           Soundness, literal & clause orderings, saturation (1)

           Model construction (1)

           Unication for general resolution (1)

           Basic general resolution, ordering & selection refinements (2)

           Redundancy elimination (1)

           Using SPASS (lab)

      * Verification

           LTL (1)

           bounded model checking (1)

Recommended reading

COMP60332 reading list can be found on the School of Computer Science website for current students.

Feedback methods

Exercise classes; assessment and feedback on written assignments.

Study hours

  • Assessment written exam - 2 hours
  • Lectures - 24 hours
  • Practical classes & workshops - 16 hours
  • Independent study hours - 108 hours

Teaching staff

Renate Schmidt - Unit coordinator

▲ Up to the top