Skip to navigation | Skip to main content | Skip to footer
Menu
Menu

This is an archived syllabus from 2014-2015

COMP60332 Automated Reasoning and Verification syllabus 2014-2015

COMP60332 Automated Reasoning and Verification

Level 6
Credits: 15
Enrolled students: 35

Course leader: Renate Schmidt


Additional staff: view all staff

Assessment methods

  • 50% Written exam
  • 50% Coursework
Timetable
SemesterEventLocationDayTimeGroup
Sem 2 P3 Lecture 2.15 Fri 09:00 - 17:00 -
Themes to which this unit belongs
  • Reasoning and Optimisation

Overview

Logic and reasoning plays an important role in computer science and practical areas of computing such as software and hardware verification, program analysis, security, semantic web and AI. For example, in web and agent technologies logical and automated reasoning methods are used for the intelligent processing of large ontologies, for decision making based on knowledge bases of structured data, and for formal specification and verification of web services. Another application of logic and automated reasoning is in software and hardware verification, in particular, automated reasoning tools are successfully used in large software and hardware companies such as Intel and Microsoft. An important part of the systems development process concerns reasoning about the behaviour of systems in order to verify the correctness of the behaviour. The main motivation of the course is the study and development of general and efficient techniques, which form the basis of state-of-the-art automated reasoning systems and verification tools.

Aims

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

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 to logics and applications (1)
  • Orderings, multi-sets, induction (1)
  • Propositional logic (2)
    • syntax, semantics, truth tables
    • concepts and results of soundness and completeness, decidability
  • Transformations to normal forms (1)
    • CNF, NNF, clauses
  • Propositional reasoning methods (4)
    • Propositional resolution, resolution rule, factoring rule, proofs
    • DPLL and SAT-solving, unit propagation, backtracking, backjumping, lemma learning
  • First-order logic (4)
    • the language of first-order logic
    • substitutions
    • normal forms, clauses, optimised normal forms
  • Semantics of first-order logic (3)
    • Herbrand models
    • concepts and results of soundness and completeness
    • orderings, model building
  • Resolution theorem proving (4) 
    • unifiers, unification algorithm
    • basic first-order resolution, ordering and selection refinements
    • redundancy elimination, distributed reasoning as application
    • Using SPASS
  • Verification (2)
    • hardware verification

Teaching 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

Feedback methods

Exercise classes; assessment and feedback on written assignments.

Study hours

Employability skills

  • Analytical skills
  • Problem solving
  • Research
  • Written communication

Learning outcomes

On successful completion of this unit, a student will be able to:

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

Reading list

TitleAuthorISBNPublisherYear
Mathematical Logic for Computer Science Ben-Ari, Mordechai. author.9781447141297Springer London2012
First-order logic and automated theorem proving Fitting, Melvin, 1942-9780387945934Springerc1996.
The essence of logic Kelly, John, 1940-0133963756Prentice Hallc1997.
Logic for Computer Scientists Schöning, Uwe. author.9780817647636Birkhäuser Boston2008
The Calculus of Computation : Decision Procedures with Applications to Verification Bradley, Aaron R. author.9783540741138Springer Berlin Heidelberg2007
Decision procedures : an algorithmic point of view Kroening, Daniel,9783662504970; 3662504979Springer2016.

Additional notes

Course unit materials

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