Brief outline of the structure of the programme and its assessment methods:
(see guidance notes)
Students take eight modules over term 1 and term 2. They have examinations in May. They undertake a dissertation June-September.
Board of Examiners:
Name of Board of Examiners:
Board of Examiners of the M.Sc. in Logic, Semantics and Verification of Programs.
Professional body accreditation
(if applicable):
N/A
Date of next scheduled accreditation visit:
EDUCATIONAL AIMS OF THE PROGRAMME:
Theoretical research is a vital part of the study of computation. UCL CS has a strong research group in computer theory. Opportunities for advanced training in computer theory are very limited in the UK, this programme will provide that opportunity.
Software verification is a worldwide pressing challenge, given our modern trend towards more software everywhere. Airplanes, phones, etc rely on the correctness of complex software. Challenges such as big data and distributed systems, entertained by the modern trend towards more efficiency and concurrency, are difficult not only to implement but also to design and reason about. For commercial and sometimes safety critical reasons, we need to be able to prove that the systems we build are correct.
We propose to form a new generation of students to be able to think deeply about the correctness of systems.
We offer foundational courses to form graduates to become engineers and researchers with a practical mindset, but with competences in formal verification of the software that they develop.
PROGRAMME OUTCOMES: The programme provides opportunities for students to develop and demonstrate knowledge and understanding, qualities, skills and other attributes in the following areas: Theory of automata and transition systems.
Modelling systems ranging from: finite state (automata), sequential (interprocedural), concurrent (shared memory, message passing), and distributed systems
Empirical understanding of how such systems actually behave when implemented in practice
Concurrency as it appears in deployed systems such as multiprocessors and GPUs
Establishing formal complexity bounds on resources used by programs (e.g. time and memory)
Fundamentals of modal and temporal logics, as well as algebras of transition systems
Verification games and computations, representations, decidability
Use of logic to formally reason about program behaviours
Automated reasoning techniques, and their application to the analysis and verification of computer programs
How to test and prove the correctness of systems with respect to a specification, both with and without the aid of tools
Teaching/learning methods and strategies:
The programme will be based on:
Primary material taught through lectures and discussions within class time. Lectures will introduce the fundamental principles and techniques of computer theory, illustrated through examples and, where appropriate, illustrations based on real-world use cases.
Practicals and tutorials, ensuring hands-on experience applying existing tools, with an emphasis on applications dealing with current systems which are actually being deployed in practice.
Reading recent research work, including seminars to discuss and debate the current state of the art in program verification.
Projects will also require the students to apply their knowledge in order to solve more open ended current challenges.
Assessment:
Examinations, oral presentations, written reports, and projects
Intellectual (thinking) skills: Analysis of complex problems and development of novel solutions
Critical awareness of the practical quality of a theoretical solution
Deep understanding of the theoretical foundations of computer systems
Critical and formal reasoning at multiple levels of abstraction
Ability to effectively translate theoretical concepts into practical applications
Listen to and discuss ideas, get acquainted with current research trends
Teaching/learning methods and strategies:
These skills are developed largely as a result of in-class discussions, project supervision, and other face-to-face meetings.
Seminars, tutorials and practicals involve the student in an active role where these intellectual skills are developed.
Assessment:
Although written examinations will be formulated in such a way so that students have to demonstrate their critical thinking skills; intellectual skills will be mainly assessed through oral presentations and project reports.
C: Skills and other attributes
Practical skills (able to): Apply and compose several tools in order to test and verify program correctness
Develop tools implementing theoretical solutions, in order to assess their practicality
Competence in programming and designing meaningful experiments
Communicate technical and scientific information effectively, both orally and in writting.
Locate and critically analyse appropriate research literature
Teaching/learning methods and strategies:
Lab sessions, programming exercises, and projects.
Written project reports as well as oral presentations at seminars.
Assessment:
Individual and group assignments, practicals, projects
D: Skills and other attributes
Transferable skills (able to): Prepare and present effective oral presentations
Present technical material effectively in written form.
Critical and constructive views of diverse theories
Relate abstract theoretical concepts to concrete empirical phenomena
Written research projects and oral presentations, with constant feedback from tutors and lecturers.
The emphasis of the programme is on students being able to understand deep theoretical concepts, and how these relate to applications actually deployed in practice.
Several projects, seminars and discussions will all develop the students abilities to work individually and as a team.
As the programme is quite intense and pressured, students are expected to organize themselves in an effective manner. Constant monitoring and feedback will be provided.
Assessment:
This skills are all implicitly assessed through individual and group assignments, practicals, projects, and oral presentations.
The following reference points were used in designing the programme:
the Framework for Higher Education Qualifications: (http://www.qaa.ac.uk/en/Publications/Documents/qualifications-frameworks.pdf);
the programme specifications for UCL degree programmes in relevant subjects (where applicable);
UCL teaching and learning policies;
staff research.
Please note: This specification provides a concise summary of the main features of the programme and the learning outcomes that a typical student might reasonably be expected to achieve and demonstrate if he/she takes full advantage of the learning opportunities that are provided. More detailed information on the learning outcomes, content and teaching, learning and assessment methods of each course unit/module can be found in the departmental course handbook. The accuracy of the information contained in this document is reviewed annually by UCL and may be checked by the Quality Assurance Agency.
Programme Organiser(s) Name(s):
Dr Alexandra Silva
Date of Production:
3 December 2013
Date of Review:
July 2016
Date approved by Chair of Departmental Teaching Committee:
