Computer Science at Oxford

From Computer Science at Oxford

Third year

Students in the third year of the Computer Science course spend between 50% and 75% of their time on advanced options, choosing between four and six of the courses. Students studying Mathematics and Computer science may choose up to six of these courses in their third year, occupying up to 75% of their time, and a further four to six in their fourth year, depending on whether they choose to do a project.

The list of options varies from year to year according to the research interests of teaching staff, but the following examples illustrate courses that have been offered recently.

Computer-Aided Formal Verification

Computer-aided formal verification aims to improve the quality of digital systems by using logical reasoning, supported by software tools, to analyse their designs. The idea is to build a mathematical model of a system and then try to prove properties of it that validate the system's correctness – or at least help discover subtle bugs. The proofs can be millions of lines long, so specially-designed computer algorithms are used to search for and check them.

This course provides a survey of several major software-assisted verification methods, covering both theory and practical applications. The aim is to familiarise students with the mathematical principles behind current verification technologies and give them an appreciation of how these technologies are used in industrial system design today.

Computational Complexity

This course is an introduction to the theory of computational complexity and standard complexity classes. One of the most important insights to have emerged from Theoretical Computer Science is that computational problems can be classified according to how difficult they are to solve. This classification has shown that many computational problems are impossible to solve, and many more are impractical to solve in a reasonable amount of time. To classify problems in this way, one needs a rigorous model of computation, and a means of comparing problems of different kinds. We introduce these ideas in this course, and show how they can be used.

Computer Security

Security aspects of computer systems have far-reaching implications in an increasingly networked world. In this course we will cover the principles underlying computer security, the problems that must be solved, and some of the solutions that are used in implementing secure systems. The course includes the use of formal models based on logic to model security problems and to verify proposed solutions.

Geometric Modelling

This is an introductory course in modelling techniques for 3D objects. It covers a wide range of different ways of representing the geometry of real objects, depending on their functionality and application. The emphasis in this course will be on the theory and basic principles of constructing models; hence the practicals will not use CAD-specific software, but rather a programming environment suitable for reasoning about the mathematics of models.

Intelligent Systems

The development of "intelligent" software systems is an area that is becoming increasingly important in applied Computer Science. It is easier to give examples such systems than to define the word "intelligent". Some instances are programs that assist users or adapt to their behaviour; identify interesting patterns in databases like those generated by the Human Genome Project; and predict stock-market movements. It is possible to abstain from any controversy on what does, or does not, constitute "intelligence and concentrate instead on the primary mathematical and computational tools necessary to develop systems capable of adaptive behaviour in complex real-world environments.

The course aims to teach you the principal issues that arise in the theory, implementation and application of intelligent software systems. Here "intelligent systems will be taken to mean those that have the ability to represent and reason with real-world tasks given limited computational resources. You will be made aware of recent developments in the fields of probabilistic modelling, machine learning and natural language processing. Some or all of these will be unavoidable requirements in the development of complex intelligent systems.

Knowledge Representation & Reasoning

Further information to follow.

Lambda Calculus and Types

Further information to follow.

Machine Learning

Further information to follow.

Principles of Programming Languages

Further information to follow.

Fourth year

In the fourth year, students spend 63% of their time on advanced options. The list of fourth-year options may vary from year to year, depending on research interests of the available staff. Here are some of the options that have been offered recently:

Advanced Security

Details to follow.

Automata, Logic and Games

This course introduces the mathematical theory underpinning the Computer-Aided Verification of computing systems. The main ingredients are:

• Automata (on infnite words and trees) as a computational model of state-based systems.
• Logical systems (such as temporal and modal logics) for specifying operational behaviour.
• Two-person games as a conceptual basis for understanding interactions between a system and its environment.

Categories, Proofs and Processes

Category Theory is a powerful mathematical formalism which has become an important tool in modern mathematics, logic and computer science. One main idea of Category Theory is to study mathematical 'universes', collections of mathematical structures and their structure-preserving transformations, as mathematical structures in their own right, i.e., categories - which have their own structure-preserving transformations (functors). This is a very powerful perspective, which allows many important structural concepts of mathematics to be studied at the appropriate level of generality, and brings many common underlying structures to light, yielding new connections between apparently different situations.

Computational Linguistics

The aim of this series of lectures is to provide an introduction to some of the major topics in computational linguistics. No previous knowledge of linguistics is required. By the end of this lecture series you should understand what the concerns of computational linguists are and be familiar with some of the major topics in the area. You should also be in a position to find out more of the practical details for yourself.

Computer Animation

Whereas the Geometric Modelling and Graphics courses described how objects are modelled and displayed on a modern computer system, Computer Animation explains how objects are set up and moved in virtual worlds. Topics include the movement of objects, both by hand and by physical simulation; the arrangement of controls for a complex object, like a human figure; the use of a modern animation system (Blender); algorithms for collision detection; and techniques for computing collision responses.

Students completing the course will have outline knowledge of the key theoretical and practical issues involving animation, and be ready to apply their skills in areas such as traditional animation, physical simulation, and computer games. Assessment is by a mix of examination-style questions and the completion of a mini-project in Blender.

Database Systems Implementation

This course examines the data structures and algorithms underlying database management systems such as Oracle or PostgreSQL. It covers techniques from both research literature and commercial systems. At the end of this course, students should have a good insight into how DBMSs function internally, and understand how to analyse the performance of data-intensive systems. They will become familiar with a variety of programming techniques for large-scale data manipulation, and be able to apply the insights achieved to build the major components of a mini-DBMS.

Information Retrieval

Information Retrieval (IR), for the purpose of this course, is the study of the indexing, processing, and querying of textual data. The growing importance of the Web means that IR has acquired added significance in recent years. The course will also look at how models of language similar to those used in IR can be applied to the problem of Machine Translation, which is becoming increasingly important as use of the Web transcends national and cultural boundaries.

The aim of the course is to provide an introduction to the basic principles and techniques used in IR; to demonstrate how statistical models of language can be used to solve the document retrieval problem; to consider specific IR applications such as cross-language retrieval; and to show how statistical models of language can be used to develop Machine Translation systems.

Probabilistic Model Checking

Probabilistic model checking is a formal technique for analysing systems that exhibit random behaviour. Examples include randomised algorithms, communication and security protocols, computer networks, biological signalling pathways, and many others. The course provides a detailed introduction to these techniques, covering both the underlying theory (Markov chains, Markov decision processes, temporal logics) and its practical application (using the state-of-the art probabilistic checking tool PRISM, based here in Oxford). The methods used will be illustrated through a variety of real-life case studies, e.g. the Bluetooth/FireWire protocols and algorithms for contract signing and power management.

Probability and Computing

Details to follow.

Program Analysis

Program analysis provides the theory, algorithms and engineering techniques to answer questions about your programs. For example, you might want to determine what statements could have contributed to the value of an expression. Another application is for a compiler to decide whether an optimisation can be applied. Or you might want some mechanical assistance when refactoring your program. Program analysis is also indispensable when proving properties of large programs, for instance to check that there are no buffer overflows.

An elegant and crisp mathematical framework is common to all these applications. This course will introduce you to that mathematics, and simultaneously show how it leads to beautiful algorithms that solve practically important problems. (Not offered in 2012/13.)

Quantum Computer Science

Both physics and computer science have been very dominant scientific and technological disciplines in the previous century. Quantum Computer Science aims at combining both and hence promises to play an important similar role in this century. Combining the existing expertise in both fields proves to be a non-trivial but very exciting interdisciplinary journey. Besides the actual issue of building a quantum computer or realizing quantum protocols it involves a fascinating encounter of concepts and formal tools which arose in distinct disciplines.

In this course, you will learn what quantum computing and quantum protocols are about, why they matter, and what are the basic scientific behind them. This includes a structural understanding of some basic quantum mechanics, knowledge of important algorithms such as Shor's algorithm and important protocols such as quantum teleportation. This course offers students a first stepping-stone for research in the field, with a particular focus on the newly developing field of quantum semantics, to which Oxford's Department of Computer Science has provided pioneering contributions.

Software Verification

The course presents a comprehensive coverage of state-of-the-art practices in software verification. It starts by a brief summary of the basics of Model Checking. We focus on industrial programming languages, that is Java and C/C++, and will discuss techniques for automatic extraction of formal models from these programming languages. We then cover abstract interpretation, bounded model checking, and predicate abstraction. At the end of the course, the students will understand the complexity and sources of complexity in modern programming languages. They will have an in-depth knowledge of modern program analysis techniques, and be aware of current research challenges in the area.

Theory of Data and Knowledge Bases

This lecture series should give you a good understanding of the fundamentals of query languages, and the trade-off between complexity and expressive power, in addition to the basic formalisms of non-monotonic reasoning. You should be in a position to analyse a query language and express knowledge in suitable logical formalisms.