Programme specification



Download 48.04 Kb.
Date05.05.2018
Size48.04 Kb.
#48147

PROGRAMME SPECIFICATION




              1. PROGRAMME SPECIFICATION




Programme title:


MSc Logic, Semantics and Verification of Programs

Final award (BSc, MA etc):

(where stopping off points exist they should be detailed here and defined later in the document)



M.Sc.

              1. UCAS code:
                (where applicable)

N/A

              1. Cohort(s) to which this programme specification is applicable:

(e.g. from 2008 intake onwards)

From 2017 onwards

Awarding institution/body:


University College London

Teaching institution:


University College London

Faculty:


Engineering

Parent Department:
(the department responsible for the administration of the programme)

Computer Science
  1. Departmental web page address:


(if applicable)


www.cs.ucl.ac.uk

Method of study:

Full-time/Part-time/Other




Full time

Criteria for admission to the programme:


An upper second class degree in mathematics, computer science, or a closely related subject.

Length of the programme:

(please note any periods spent away from UCL, such as study abroad or placements in industry)



12 months

Level on Framework for Higher Education Qualifications (FHEQ)
(see Guidance notes)

Master’s level (MSc Award): level 7

Relevant subject benchmark statement (SBS)
(see Guidance notes)

http://www.qaa.ac.uk/Publications/InformationAndGuidance/Pages/SBS-Masters-degree-computing.aspx

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.



        1. Professional body accreditation

        2. (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.

Logics and algebras of transitions.

Complexity of automated systems.

Program verification.

Concurrent systems.

Game theory and computations.




A: Knowledge and understanding


Knowledge and understanding of:

Computer theory with an empirical twist:



  1. How to formalise the behaviour of computer programs by means of transition systems

  2. Modelling systems ranging from: finite state (automata), sequential (interprocedural), concurrent (shared memory, message passing), and distributed systems

  3. Empirical understanding of how such systems actually behave when implemented in practice

  4. Concurrency as it appears in deployed systems such as multiprocessors and GPUs

  5. Establishing formal complexity bounds on resources used by programs (e.g. time and memory)

  6. Fundamentals of modal and temporal logics, as well as algebras of transition systems

  7. Verification games and computations, representations, decidability

  8. Use of logic to formally reason about program behaviours

  9. Automated reasoning techniques, and their application to the analysis and verification of computer programs

  10. 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


    1. B: Skills and other attributes





Intellectual (thinking) skills:

  1. Analysis of complex problems and development of novel solutions

  2. Critical awareness of the practical quality of a theoretical solution

  3. Deep understanding of the theoretical foundations of computer systems

  4. Critical and formal reasoning at multiple levels of abstraction

  5. Ability to effectively translate theoretical concepts into practical applications

  6. 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.


    1. C: Skills and other attributes





Practical skills (able to):

  1. Apply and compose several tools in order to test and verify program correctness

  2. Develop tools implementing theoretical solutions, in order to assess their practicality

  3. Competence in programming and designing meaningful experiments

  4. Communicate technical and scientific information effectively, both orally and in writting.

  5. 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


    1. D: Skills and other attributes





Transferable skills (able to):

  1. Prepare and present effective oral presentations

  2. Present technical material effectively in written form.

  3. Critical and constructive views of diverse theories

  4. Relate abstract theoretical concepts to concrete empirical phenomena

  5. Work effectively both independently and in a group

  6. Manage time effectively



Teaching/learning methods and strategies:

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 relevant Subject Benchmark Statements

(http://www.qaa.ac.uk/assuring-standards-and-quality/the-quality-code/subject-benchmark-statements);

  • 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:

July 2016

Date approved by Faculty Teaching Committee


July 2016


Download 48.04 Kb.

Share with your friends:




The database is protected by copyright ©ininet.org 2024
send message

    Main page