MSc ACS: Computer Security

Year of entry: 2020

Course unit details:
Automated Reasoning and Verification

Unit code COMP60332
Credit rating 15
Unit level FHEQ level 7 – master's degree or fourth year of an integrated master's degree
Teaching period(s) Semester 2
Offered by Department of Computer Science
Available as a free choice unit? Yes

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.

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.

Learning outcomes

  • A basic understanding of the computational needs of modern biology.

  • Develop an understanding of the problems inherent in communicating with scientists  from a different discipline.

  • Develop the ability to reflect upon and synthesize a range of computational techniques to develop effective problem solving strategies in an unfamiliar problem domain.

  • Develop the ability to communicate these strategies to non-specialists.

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)

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

Employability skills

Analytical skills
Problem solving
Research
Written communication

Assessment methods

Method Weight
Written exam 50%
Written assignment (inc essay) 50%

Feedback methods

Exercise classes; assessment and feedback on written assignments.

Recommended reading

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

Study hours

Scheduled activity hours
Assessment written exam 2
Lectures 24
Practical classes & workshops 16
Independent study hours
Independent study 108

Teaching staff

Staff member Role
Renate Schmidt Unit coordinator

Additional notes

Course unit materials

Links to course unit teaching materials can be found on the School of Computer Science website for current students.

Return to course details