Module COMP4127: AUTOMATED REASONING AND VERIFICATION

Department: Computer Science

COMP4127: AUTOMATED REASONING AND VERIFICATION

Prerequisites

• COMP2181 Theory of Computation

Corequisites

Excluded Combination of Modules

Aims

• To introduce students to Automated Reasoning through expression and solvability of problems in propositional and first-order logic.
• To introduce students to Verification through expression and solvability of problems using temporal logics.
• To introduce students to Program Correctness through Hoare Logic.

Content

• Algorithms for Reasoning in Propositional Logic
• Principles of Modern SAT Solvers
• Algorithms for Reasoning in First Order Logic
• Unification and Resolution for First Order Logic
• Principles of Inference in Prolog
• Transition Systems and Model-Checking
• Linear Temporal Logic
• Computation Tree Logic
• Model-Checking with NuSMV
• Hoare Logic

Learning Outcomes

• On completion of the module, students will be able to demonstrate:
• an understanding of how to express problems in the language of logics and models.
• an understanding of satisfiability, entailment and model-checking for a variety of logics.
• an understanding of the algorithms underlying modern SAT-solvers.
• an understanding of the algorithms underlying verification in temporal logics.
• an understanding of how a program can be proved to meet a specification through Hoare Logic.

• On completion of the module, students will be able to demonstrate:
• an ability to refute unsatisfiable propositional clause sets with Resolution.
• an ability to refute unsatisfiable first-order sentences through First-Order Resolution.
• an ability to work with modern SAT-solvers and NuSMV
• an ability to prove a program correct using Hoare Logic

• On completion of the module, students will be able to demonstrate:
• an ability to formalise computational problems in a variety of contexts.
• an ability to reason mathematically about information, systems and programs in a variety of ways.

Modes of Teaching, Learning and Assessment and how these contribute to the learning outcomes of the module

• Lectures enable the students to learn new material relevant Automated Reasoning and Verification.
• The examination assesses an understanding of core concepts.

Teaching Methods and Learning Hours

Summative Assessment

Formative Assessment:

Example formative exercises are given during the course.

■ Attendance at all activities marked with this symbol will be monitored. Students who fail to attend these activities, or to complete the summative or formative assessment specified above, will be subject to the procedures defined in the University's General Regulation V, and may be required to leave the University