MSc ACS: Computer Security
Year of entry: 2020
Course unit details:
Automated Reasoning and Verification
|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|
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.
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.
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.
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)
+ LTL (1)
+ bounded model checking (1)
Teaching and learning methods
Lecturers will be interspersed with example classes and labs on teaching days
Example classes will take place on teaching days
Labs will take place on teaching days
- Analytical skills
- Problem solving
- Written communication
|Written assignment (inc essay)||50%|
Exercise classes; assessment and feedback on written assignments.
COMP60332 reading list can be found on the School of Computer Science website for current students.
|Scheduled activity hours|
|Assessment written exam||2|
|Practical classes & workshops||16|
|Independent study hours|
|Renate Schmidt||Unit coordinator|
Course unit materials
Links to course unit teaching materials can be found on the School of Computer Science website for current students.