MSc Machine Learning

The course unit aims to provide a foundation for formal methods in software verification, software security, software engineering and computer science. Formal methods heavily rely on automated reasoning which will be the central focus of the course. It covers basic mathematical foundations and formalisms to model and reason about different aspects of complex systems and programs. In laboratory sessions students gain practical experience for the use of state-of-the art automated reasoning tools that are widely used for formal methods and verification of security protocols and programs.

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.

1. Describe and compare approaches to modelling and representation of knowledge in logical form in propositional logic and first-order logic.

2. Describe and compare approaches underpinning modern automated reasoning and verification systems. 

3. Explain techniques that make such systems efficient and suitable to verify large pieces of software.

4. Formalise and describe properties of relations, the specification of a program, a security protocol or constraints of a combinatorial problem. 

5. Solve a variety of reasoning problems in software verification and security protocol analysis.

6. Use a state-of-the art first-order reasoner to establish properties of relations and analyse a security protocol. 

7. Use a state-of-the-art SAT/SMT solver to verify properties of data structures.

8. Independently study a chosen relevant topic which may involve contrasting different approaches to modelling and reasoning, applying reasoning approaches to a special fragment or evaluating an advanced reasoning technique.

- Introduction


- Propositional reasoning

• Language of propositional logic, semantics, truth tables
• Satisfiability, validity, equivalence, decidability
• Normal forms, CNF, clauses
• Propositional resolution, redundancy elimination
• DPLL and CDCL for SAT-solving
• Logical modelling
• Using SAT solver (demo & lab)
   

- General first-order reasoning

• Language of first-order logic, modelling
• substitution, semantics
• Normal forms, clauses
• Herbrand interpretations
• Soundness, literal & clause orderings, saturation
• Unication for general resolution
• Basic general resolution, ordering & selection refinements
• Automated analysis of security protocols
• Using SPASS (demo & lab)
   

- Reasoning modulo theories (SMT)

• Equality reasoning, theory of arrays, linear arithmetic, SMT algorithm
• Property checking related to software
• Using SMT solver (demo & lab)

Delivery and learning are via a range of materials and sessions: video lectures, quizzes, flipped classroom sessions, drop-in sessions, feedback sessions and supervised practical laboratory sessions.

Lecture notes are made available online. Together with the videos and the slides of the flipped classroom sessions they comprise the formal content of the course unit. The videos explain the material more informally with emphasis on key concepts, examples and exercises.

The practical work involves learning to use and getting experience with current reasoners and systems used for program verification and analysis. These systems will be used in the Software Security course unit.

Other:

Assessed coursework 35%

Assessed practical work 15%

Mini-Project (formative)

For assessed coursework there are face-to-face sessions with GTAs in which cohort-level feedback is provided on common mistakes along with marks.

Each practical assessment piece is checked, and face-to-face cohort level feedback is provided in feedback sessions along with marks.

Individual feedback is provided in feedback sessions on formative mini-projects.

For the exam cohort level feedback is given along with individual marks after marking and official exam board meetings.

Mathematical Logic for Computer Science

Ben-Ari, Mordechai, 2012. Springer, London

The Calculus of Computation: Decision Procedures with Applications to Verification 

Bradley, Aaron R. and Manna, Zohar, 2007. Springer, Berlin/Heidelberg

Other non-listed Scheduled activities for Scheduled activity hours:

• Coursework drop-in sessions 5 hours
• Coursework feedback sessions 5 hours
• Exam revision Q&A Session 2 hours

Additional information regarding Non-scheduled/Independent study hours:

• Video content 20 hours
• Coursework 30 hours

More information regarding this Unit:

• This is a Mandatory course in Secure Software Engineering Theme and MSc in Cyber Security
• Please contact the unit lead to get permission to do the unit if you are not a Comp Sci student/ unable to enrol onto the unit.