One of the few masters degrees available with a focus on the area between formal logic and theoretical computer science, MSc in Logic, Semantics, and Verification of Programs at UCL is a new programme providing an excellent opportunity to study highly theoretical aspects of computer science with a practical application in program verification.

The main focus of this degree is in logic, semantics, and their applications in program verification, but the more general problem addressed in this degree is an analysis of the correctness of systems.  Students are presented with up to date techniques in this area and develop problem solving skills involving abstract models of logics and programs.

Program verification is an increasingly important area. Software bugs and security vulnerabilities can cause enormous costs and risks and for that reason a large number of companies is now investing in building correct software. This MSc will equip students with basic knowledge to  build software that does what it is supposed to do and, moreover, with techniques to analyse and prove software correct. This MSc is organised by the Principles of Programming, Logic, and Verification group, who has strong links with leading companies including Facebook and Microsoft, in addition to other digital companies with an interest in program verification, who will engage with students throughout the course. The degree may also lead some graduates into a PhD program, either at UCL or elsewhere.

 

The programme consists of four core modules (60 credits), four optional modules (60 credits) and a research project (60 credits). All MSc students undertake an independent research project which culminates in a dissertation in the form of a project report.

Students can take up to one postgraduate module from elsewhere in UCL as part of their options. All choices are subject to timetabling constraints and the approval of the relevant Module Tutor and the Programme Director.

Core Modules

COMPGL02 Logic of Programs and Transition Systems

COMPGL02 Logic of Programs and Transition Systems

This course introduces various formal methods of reasoning about transition systems. The course covers Modal, Temporal as well as algebras of transition systems. Students are taught how to establish complexity bounds on programs and transition systems.

Full syllabus coming soon.

COMPGL03 Program Verification and Automated Reasoning

COMPGL03 Program Verification and Automated Reasoning

This course covers various aspects of program verification, including higher-order and concurrent programs.

Full syllabus coming soon. 

COMPGS03 Validation and Verification

COMPGS03 Validation and Verification

The module will train students in the principles and techniques of validating and verifying software systems. The training will be intellectually demanding and will cover not only the state-of-the practice in validation and verification, but also the most significant trends, problems and results in validation and verification research.

Further syllabus information can be found here.

Optional Modules

COMPGI01 Supervised Learning

COMPGI01 Supervised Learning

This module covers supervised approaches to machine learning. It starts by reviewing fundamentals of statistical decision theory and probabilistic pattern recognition followed by an in-depth introduction to various supervised learning algorithms such as Perceptron, Backpropagation algorithm, Decision trees, instance-based learning, support vector machines. Algorithmic-independent principles such as inductive bias, side information, approximation and estimation errors. Assessment of algorithms by jackknife and bootstrap error estimation, improvement of algorithms by voting methods such as boosting. Introduction to statistical learning theory, hypothesis classes, PAC learning model, VC-dimension, growth functions, empirical risk minimization, structural risk minimization.

Students will gain an in-depth familiarity with various classical and contemporary supervised learning algorithms, understand the underlying limitations and principles that govern learning algorithms and ways of assessing and improving their performance, understand the underlying fundamentals of statistical learning theory, the complexity of learning and its relationship to generalization ability.

Further syllabus information can be found here.

COMPGI07 Programming & Mathematical Methods for Machine Learning

COMPGI07 Programming & Mathematical Methods for Machine Learning

The aims of the module are to provide a practical knowledge and understanding of the programming environments of Matlab and Mathematica. Knowledge of and proficiency in these languages/packages form an essential component of courses GI06 (Evolutionary Systems) and GI01 (Supervised Learning). The aim is also to introduce students to those elements of linear algebra which play an important role in machine learning and data analysis.

Further syllabus information can be found here.

COMPGS10 Language Based Security

COMPGS10 Language Based Security

This module provides students with specialist knowledge and understanding to solve software related problems associated with the security of software systems. Students discover the relationship between computer program design and security, how various security-related properties of computer programs are formulated and guaranteed, and in-depth knowledge of a variety of contexts in which understanding can be applied.

Further syllabus information can be found here.

COMPGV01 Mathematical Methods Algorithms & Implementations

COMPGV01 Mathematical Methods Algorithms & Implementations

To provide a rigorous mathematical approach: in particular to define standard notations for consistent usage in other modules. To present relevant theories and results. To develop algorithmic approach from mathematical formulation through to hardware implications.

Further syllabus information can be found here.

COMPGA03 Introduction to Cryptography

COMPGA03 Introduction to Cryptography

This modules provides students with the foundations of cryptography and information security. We introduce the main security properties needed in today's systems, such as confidentiality, authentication, integrity, anonymity, non-repudiation, and do so by means of rigorous definitions and formal assumptions. The module then covers state-of-the-art technologies to meet these goals, i.e., pseudorandomness, encryption, digital signatures, message authentication codes, hash functions.

Further syllabus information can be found here.

COMPGV11 Geometry of Images

COMPGV11 Geometry of Images

The aim of this module is to introduce the generalisation of image processing to n-Dimensional data: volume data, scale space, time-series and vectorial data. Students will understand the principles of image processing in n-dimensions, time-series analysis and scale space, and to understand the relations between geometric objects and sampled images.

Further syllabus information can be found here.

MATHMM04 Computational and Simulation Methods

MATHMM04 Computational and Simulation Methods

This module is taught by the Department of Mathematics.

Further syllabus information can be found here.

MSc Logic, Semantics and Verification of Programs comprises 8 taught modules and a Research Project. Of the taught modules, 3 are core modules, with at least 3 optional modules and a combination of optional and elective modules for the remainder.

Core Modules

COMPGL01 Introduction to Logic, Semantics and Verification

COMPGL01 Introduction to Logic, Semantics and Verification

Further syllabus information will be available shortly.

COMPGL02 Logic of Programs and Transition Systems

COMPGL02 Logic of Programs and Transition Systems

Further syllabus information will be available shortly.

COMPGL03 Program Verification and Automated Reasoning

COMPGL03 Program Verification and Automated Reasoning

Further syllabus information will be available shortly.

COMPGL99 Research project

COMPGL99 Research project

Further syllabus information will be available shortly.

Optional Modules

COMPGA03 Introduction to Cryptography

COMPGA03 Introduction to Cryptography

This modules provides students with the foundations of cryptography and information security. We introduce the main security properties needed in today's systems, such as confidentiality, authentication, integrity, anonymity, non-repudiation, and do so by means of rigorous definitions and formal assumptions. The module then covers state-of-the-art technologies to meet these goals, i.e., pseudorandomness, encryption, digital signatures, message authentication codes, hash functions.

Further syllabus information can be found here.

COMPGL04 Verification and Mechanised Proofs

COMPGL04 Verification and Mechanised Proofs

Further syllabus information will be available shortly.

COMPGS03 Validation and Verification

COMPGS03 Validation and Verification

The module will train students in the principles and techniques of validating and verifying software systems. The training will be intellectually demanding and will cover not only the state-of-the practice in validation and verification, but also the most significant trends, problems and results in validation and verification research.

 

Further syllabus information can be found here.

COMPGS10 Language Based Security

COMPGS10 Language Based Security

This module provides students with specialist knowledge and understanding to solve software related problems associated with the security of software systems. Students discover the relationship between computer program design and security, how various security-related properties of computer programs are formulated and guaranteed, and in-depth knowledge of a variety of contexts in which understanding can be applied.

Further syllabus information can be found here.

COMPGV01 Mathematical Methods Algorithms & Implementations

COMPGV01 Mathematical Methods Algorithms & Implementations

To provide a rigorous mathematical approach: in particular to define standard notations for consistent usage in other modules. To present relevant theories and results. To develop algorithmic approach from mathematical formulation through to hardware implications.

 

Further syllabus information can be found here.

COMPGV11 Geometry of Images

COMPGV11 Geometry of Images

The aim of this module is to introduce the generalisation of image processing to n-Dimensional data: volume data, scale space, time-series and vectorial data. Students will understand the principles of image processing in n-dimensions, time-series analysis and scale space, and to understand the relations between geometric objects and sampled images.

 

Further syllabus information can be found here.

MATHGM04 Computational and Simulation methods

MATHGM04 Computational and Simulation methods

Further syllabus information can be found here.

You will need to choose a minimum of 45 and a maximum of 75 credits from the optional modules.

Elective Modules

COMPGI01 Supervised Learning

COMPGI01 Supervised Learning

This module covers supervised approaches to machine learning. It starts by reviewing fundamentals of statistical decision theory and probabilistic pattern recognition followed by an in-depth introduction to various supervised learning algorithms such as Perceptron, Backpropagation algorithm, Decision trees, instance-based learning, support vector machines. Algorithmic-independent principles such as inductive bias, side information, approximation and estimation errors. Assessment of algorithms by jackknife and bootstrap error estimation, improvement of algorithms by voting methods such as boosting. Introduction to statistical learning theory, hypothesis classes, PAC learning model, VC-dimension, growth functions, empirical risk minimization, structural risk minimization.

Students will gain an in-depth familiarity with various classical and contemporary supervised learning algorithms, understand the underlying limitations and principles that govern learning algorithms and ways of assessing and improving their performance, understand the underlying fundamentals of statistical learning theory, the complexity of learning and its relationship to generalization ability.

Further syllabus information can be found here.

COMPGI07 Programming & Mathematical Methods for Machine Learning

COMPGI07 Programming & Mathematical Methods for Machine Learning

The aims of the module are to provide a practical knowledge and understanding of the programming environments of Matlab and Mathematica. Knowledge of and proficiency in these languages/packages form an essential component of courses GI06 (Evolutionary Systems) and GI01 (Supervised Learning). The aim is also to introduce students to those elements of linear algebra which play an important role in machine learning and data analysis.

 

Further syllabus information can be found here.

You may choose up to 30 credits as elective modules.

Module Selection

The modules that make up a programme are either core, optional or elective, which reflects whether they must be taken or can optionally be taken. The programme’s curriculum (also called a programme diet) will prescribe in what combinations modules can be taken, any restrictions on doing so, and how much credit can and must be taken.

Core/compulsory modules are fundamental to the programme’s curriculum and students must take these. You will be automatically allocated a place on any core modules for your programme and will not need to select these during the module selection process. There will be no timetable clashes between your programme’s core modules.

Optional modules are strongly related to the programme and students can choose which of these they wish to take, usually from within specific groups (for example, a student may be asked to choose two optional modules from one group and three from another, etc.) Places of optional modules are strictly limited (due to spatial, resource and timetable constraints) and will be allocated on a first come first serve basis. Some optional modules have pre-requisites which students will need to meet in order to be eligible for a place.

Elective modules are not programme specific, but allow students the opportunity to explore their interests more widely. Students are usually restricted to taking one or two elective modules.There is no guarantee of being accepted onto an elective module. These modules are core and/ or optional on other programme diets, consequently students on these programmes will be given priority. Any remaining places will then be allocated on a first come first served basis. Some elective modules have pre-requisites which students will need to meet in order to be eligible for a place.

Please note: timetable clashes between optional and elective modules from different specialisations are inevitable and this can result in limiting the available choices. It is the student’s responsibility to select modules that do not clash in order to meet UCLs minimum attendance requirements. Please speak to your Programme Director and/ or Programme Administrator if you have any queries.

Non-Computer Science students should note that priority on COMP* modules will always be given to Computer Science students in the first instance.

A minimum of an upper second-class UK Bachelor's degree in a subject such as mathematics or computer science, or an overseas qualification of an equivalent standard. A fluency in mathematics and some experience of computer programming are required; familiarity with elementary logic is a great advantage.

English Language Requirements

If your education has not been conducted in the English language, you will be expected to demonstrate evidence of an adequate level of English proficiency.

The English language level for this programme is: Good

Further information can be found on our English language requirements page.

 

UK/EU fees (FT):  £11,800 for 2017/18

Overseas fees (FT): £24,140 for 2017/18

For a comprehensive list of the funding opportunities available at UCL, including funding relevant to your nationality, please visit the Scholarship and Funding website.

If you are holding an offer from the Department of Computer Science at UCL, you may be eligible for our Excellence Scholarship.

Tuition Fee Deposit

This programme requires that applicants firmly accepting their offer pay a deposit. This allows UCL to effectively plan student numbers, as students are more demonstrably committed towards commencing their studies with us.

For full details about the UCL tuition fee deposit, please see the central UCL pages.

Tuition fee deposits within the Department of Computer Science are currently listed as:

UK/EUOverseas
Full-time*Part-timeFull-time*Part-time
£2000£1000£2000£1000
 
*where part-time is an available mode of study

Employability

The Department's graduates are particularly valued as a result of the our international reputation, strong links with industry, and ideal location close to the City of London.

Top MSc graduate destinations include:       

  • Facebook
  • Microsoft
  • Dunhumby
  • ARM

Top MSc graduate roles include:                

  • Verification Engineer
  • Big Data Architect
  • SQL Developer
  • Business Analyst

Top further study destinations:

  • UCL
  • University of Cambridge
  • MIT

Average starting salary £34,120 (all data from Graduate Surveys, January 2015)

Our Principles of Programming, Logic, and Verification group has strong links with leading companies including Facebook and Microsoft, in addition to other digital companies with an interest in program verification, who will engage with students throughout the course. The degree may also lead some graduates into a PhD program, either at UCL or elsewhere.

Programme Administrator
Samantha Bottomley
Office 5.22 Malet Place Engineering Building 
+44 (0)20 7679 0328 
advancedmsc-admissions@cs.ucl.ac.uk

More information

Programme Director: Alexandra Silva

Apply

To apply now click here.

Students are advised to apply as early as possible due to competition for places. Those applying for scholarship funding (particularly overseas applicants) should take note of application deadlines.

Deadline 17 June 2017.