Undergraduate Programme and Module Handbook 2020-2021 (archived)
Module COMP4127: AUTOMATED REASONING AND VERIFICATION
Department: Computer Science
COMP4127: AUTOMATED REASONING AND VERIFICATION
| Type | Open | Level | 4 | Credits | 10 | Availability | Available in 2020/21 | Module Cap | None. | Location | Durham |
|---|
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
Subject-specific Knowledge:
- 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.
Subject-specific Skills:
- 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
Key Skills:
- 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
| Activity | Number | Frequency | Duration | Total/Hours | |
|---|---|---|---|---|---|
| lectures | 20 | 2 per week | 1 hour | 20 | |
| preparation and reading | 80 | ||||
| total | 100 |
Summative Assessment
| Component: Examination | Component Weighting: 100% | ||
|---|---|---|---|
| Element | Length / duration | Element Weighting | Resit Opportunity |
| Examination | 2 hours | 100% | No |
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