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

COMP60332 Automated Reasoning and Verification syllabus 2020-2021

COMP60332 materials

COMP60332 Automated Reasoning and Verification

Level 6
Credits: 15
Enrolled students: pending

Course leader: Renate Schmidt


Additional staff: view all staff

Assessment methods

  • 50% Written exam
  • 50% Coursework
Timetable
SemesterEventLocationDayTimeGroup
Sem 2 w20 Lecture 2.15 Fri 09:00 - 17:00 -
Sem 2 w21-24 Lecture 2.15 Fri 09:00 - 14:00 -
Sem 2 w21-24 ONLINE LabORATORY Fri 14:00 - 17:00 -
Themes to which this unit belongs
  • Software Security and Automated Reasoning
  • Computer Science units for ACSwITM students (semester 2)

Overview

This course unit detail provides the framework for delivery in 20/21 and may be subject to change due to any additional Covid-19 impact. Current students should see Blackboard/course unit related emails for any further updates.

Automated reasoning plays an important role in computer science because an incredible array of problems can be expressed as satisfiability tests or consequence queries. This means areas such as analyis, verification and security of software and hardware, knowledge engineering, AI and computational mathematics require support from automated reasoning tools. They are, for example, used in large software and hardware companies such as Microsoft and Intel for software and hardware analysis, synthesis and verification. An important part of systems development processes concerns reasoning about the behaviour of the systems in order to verify the correctness of the behaviour.  Also, in web and agent technologies 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. The motivation of the course is the introduction and study of a subset of the most important methods, techniques and tools used nowadays. These include SAT solvers, theory reasoners (SMT) and first-order reasoners.

Aims

The course aims at providing an understanding of the foundation of propositional logic, first-order logic and important theories for modelling and reasoning specifying properties of programs. It covers practical and theoretical techniques and results that form the basis of resolution reasoning systems and the DPLL reasoning algorithm, which is used in SAT and SMT solvers. Verification and automated analysis of security protocols are discussed as important application domains.  

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 (1)
      + Propositional resolution, redundancy elimination (1)
      + DPLL and SAT-solving (1)
      + Logical modelling (1)
      + Using SAT/SMT solver (demo & lab)
* General first-order reasoning
      + Language of first-order logic, modelling (2)
      + substitution, semantics (1)
      + Normal forms, clauses (2)
      + Herbrand interpretations (1)
      + Soundness, literal & clause orderings, saturation (1)
      + Model construction (1)
      + Unication for general resolution (1)
      + Basic general resolution, ordering & selection refinements (2)
* Verification
      + Reasoning modulo theories (SMT): equality, data structures (2)
      + Verification, automated analysis of security protocols (2)
      + Using SPASS (demo & lab)

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

  • Assessment written exam (6 hours)
  • Lectures (24 hours)
  • Practical classes & workshops (16 hours)

Employability skills

  • Analytical skills
  • Problem solving
  • Research
  • Written communication

Learning outcomes

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

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

  • Model information in the language of propositional logic, first-order logic, and integrated theories relevant to software verification;
  • Translate logical representations in English;
  • Describe important notions such as soundness, refutational completeness, decidability;
  • Explain relationships between satisfiability, unsatisfiability validity and equivalence (also relative to a theory), and exploit them for automated reasoning and verification;
  • Check these using truth tables, resolution, the DPLL algorithm and the DPLL(T) algorithm;
  • Describe and apply conjunctive and clausal normal form transformations;
  • Determine how sets (clauses) compare using orderings, and determine maximal elements (literals);
  • Find and determine interpretations for clauses (formulas), and compute candidate models;
  • Apply the basic unification algorithm to unify terms and atomic formulas;
  • Use orderings and selection refinements to restrict how inferences are performed in resolution;
  • Simplify and determine redundancy of clauses;
  • Use a first-order reasoner to establish properties of relations and analyse a security protocol;
  • Use a SAT/SMT solver to verify properties of data structures;

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

Additional notes

Course unit materials

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