Honour School of Computer Science - Student projects

(Joint with Mehrnoosh Sadzradeh) Contextuality is a fundamental feature of quantum physical theories and one that distinguishes it from classical mechanics. In a recent paper by Abramsky and Brandenburger, the categorical notion of sheaves has been used to formalize contextuality. This has resulted in generalizing and extending contextuality to other theories which share some structural properties with quantum mechanics. A consequence of this type of modeling is a succinct logical axiomatization of properties such as non-local correlations and as a result of classical no go theorems such as Bell and Kochen-Soecker. Like quantum mechanics, natural language has contextual features; these have been the subject of much study in distributional models of meaning, originated in the work of Firth and later advanced by Schutze. These models are based on vector spaces over the semiring of positive reals with an inner product operation. The vectors represent meanings of words, based on the contexts in which they often appear, and the inner product measures degrees of word synonymy. Despite their success in modeling word meaning, vector spaces suffer from two major shortcomings: firstly they do not immediately scale up to sentences, and secondly, they cannot, at least not in an intuitive way, provide semantics for logical words such as `and', `or', `not'. Recent work in our group has developed a compositional distributional model of meaning in natural language, which lifts vector space meaning to phrases and sentences. This has already led to some very promising experimental results. However, this approach does not deal so well with the logical words.

The goal of this project is to use sheaf theoretic models to provide both a contextual and logical semantics for natural language.  We believe that sheaves provide a generalization of the logical Montague semantics of natural language which did very well in modeling logical connectives, but did not account for contextuality. The project will also aim to combine these ideas with those of the distributional approach, leading to an approach which combines the advantages of Montague-style and vector-space semantics.

Prerequisites

==========

The interested student should have taken the category theory and 

computational linguistics courses, or be familiar with the contents of 

these.

Professor Michael Benedikt ( benedikt@comlab.ox.ac.uk) would be delighted to supervise projects in Data Cleaning. Please feel free to contact him.

This project will look at how to find the best plan for a query, given a collection of data sources with access restrictions.

We will look at logic-based methods for analyzing query plans, taking into account integrity constraints that may exist on the data.

Professor Michael Benedikt ( benedikt@comlab.ox.ac.uk) would be delighted to supervise projects in XML transformation and update languages. Please feel free to contact him.

Professor Mike Brady (department of engineering science, jmb@robots.ox.ac.uk) would be delighted to supervise projects in medical image analysis. See http://www.robots.ox.ac.uk/~mvl/external/mvl-html/

Complex systems are characterized by variety and uncertainty. A heterogeneous agent-based modelling approach to such systems would need to specify the types of agents, their properties, the structure of the network, and the information flows among them. Generic and domain-specific research questions could be investigated within this context. This topic could be adapted to the student's background and interests. From a theoretical perspective, the project could aim to produce a formal specification of properties of such as adaptiveness, emergence and robustness. From a more applied perspective, the project could implement and extend existing approaches to modelling complex systems such as the Internet, biological systems and financial markets.

Prerequisites:

Intelligent Systems or Machine Learning
At least one of: Introduction to Specification (MSc), Probability and Computing, or Probabilistic Model Checking

Please feel free to contact Dr Ani Calinescu to discuss any of these project topics in more detail.

This topic involves the specification, implementation and analysis of algorithms and protocols, in order to investigate, prove and validate properties of pervasive computing systems. Examples include electronic voting protocols and human authentication protocols.

Prerequisites:

Computer Security and (Concurrent Programming and/or Concurrency)

Please feel free to contact Dr Ani Calinescu to discuss any of these project topics in more detail.

The simulation of objects and beings within a computer has become a hot topic over the last few years, with applications to virtual reality, the design of safe stadia, synthetic actors and environments for films, and computer games, amongst others. This project would look at the design and construction of a relatively simple animation or simulation system, that would probably sacrifice ease of animation in order to focus on the modelling of interactions between the actors and their environments.

Such a project would probably make use of existing collision detection code within the computing laboratory, coupled with algorithms that simulate the physical interaction of bodies. (An alternative would be to use one of the physical modelling APIs that are now becoming available.)

A robot cannot find its way by looking at a map designed for humans; rather, it must make a complex series of geometric calculations. Many algorithms have been developed for robot path planning, and the purpose of this project is to investigate (and improve upon) some of these. The `robot' might be an arbitrary convex polygon that can slide in a world composed of polygonal obstacles; an industrial robot arm; or a human trying to find their way across a strange city.

Which algorithm(s) you investigate is largely up to you: they range from pragmatic, `suck-it-and-see' methods to mathematically-complicated methods that are guaranteed to succeed (after a lot of CPU time!). There is also considerable scope to think of novel robots. For example, previous groups have considered:

• a planetary exploration vehicle;
• a smart torpedo;
• and a model railway track.

For several years now FIRA (Federation of International Robot-Soccer Association) has promoted the development of robot soccer, with the stated goal of producing a team of robots that can play (and beat!) humans by the year 2050. Their main events are tournaments in which research teams play each other using small wheeled robots, but more recently they have introduced a simulation league (`Simurosot'), in which a simulation server program is provided as the `playing surface'. The programmers then construct their teams as client programs, and two such teams can then play each other with the server acting a referee and providing an overhead view of the play.

The key to producing a (simulated) robot team is deciding how each player will move in response to (a) its position relative to the ball and goals, and (b) the positions of the other players --- this information is provided to both teams by the server on each cycle. Robot soccer is in its infancy, and most play is laughable; in order to produce interesting play it is necessary to encode {\em strategy} and {\em tactics}, and so it is expected that most of the effort in this project would focus on providing such a capability. Apart from that, the project is open-ended; a really interesting (but difficult!) extension of this project would have your team capable of learning about your opponent's tactics, and reacting to them!

Requirements No physical robots need be touched to do this project. The FIRA server as supplied runs on PCs under Windows, and similar servers are available for Linux. Team strategy can be encoded in a standard language (e.g., C), or using a language that is designed for describing agents.

This project will be more fun if multiple teams are constructed, so that they can play each other!

Links I've constructed a web-page for robot soccer links at: http://www.comlab.ox.ac.uk/~cameron/soccer/, which includes links to the FIRA site and the basic rules of the game.

The aim of this project is to produce a system on which it is possible to design and render (display) a complicated surface, of the sort used in many graphics systems. These surfaces are defined by a number of points in space, with the surface itself fitting smoothly between these points. Thus the required system must make it easy for the user to define these points. This can be done by starting with a regular array of points in a plane, which the user can tweak using the computer's mouse. To be useful as a design tool the system should be totally interactive: the user should be able to use the windowing system to view the grid of control points from any viewing angle, using icons to control the interaction. When the user is satisfied with the set of control points he should be able to see a display of the smooth surface itself.

Several variations of this project are possible, depending on the way that the graphical user interface is constructed, the types of surfaces considered, and the degree of realism in the display of the surface.

The system could be written on some machine that you have easy access to (e.g., a PC), or using a Sun (in which case it would probably have to be written in C or Java to make full use of the Sun graphics)

Bob Coecke is willing to supervise projects in these areas. Please feel free to contact him.

- Quantum computing and quantum information
- Category theory in logic and physics
- Diagrammatic languages in computer science, logic and physics
- Distributional compositional models of meaning
- Domain theory and probability
- Foundations of computing and physics 

(Joint with Michael Goldsmith) Kinect interface development for cybersecurity visual analytics tool: using the open development environment for Kinect, to develop an alternative HCI for the Oxford CyberVis tool http://www.cs.ox.ac.uk/projects/cybervis/ (focusing on navigation of the CyberVis environment). As CyberVIs is primarily developed in JAVA a good understanding that language is essential in order to interface Kinect to CyberVis. Suitable for 3rd or 4th year undergraduates, or MSc. Other projects on novel human-computer interfaces for security possible, depending on interest and inspiration.

(Joint with Michael Goldsmith)

Modelling of security-related interactions, in CSP or more evocative notations such as Milner's bigraphs (http://www.springerlink.com/content/axra2lvj4ph81bdm/; http://www.amazon.co.uk/The-Space-Motion-Communicating-Agents/dp/0521738334/ref=sr_1_2?ie=UTF8&qid=1334845525&sr=8-2). Concurrency and Computer Security a distinct advantage. Appropriate for good 3rd or 4th year undergraduates or MSc. * Open to suggestions for other interesting topics in Cybersecurity, if anyone has a particular interest they would like to pursue.

(Joint with Michael Goldsmith)

Smartphone security: one concrete idea is the development of a policy language to allow the authors of apps to describe their behaviour, designed to be precise about the expected access to peripherals and networks and the purpose thereof (data required and usage); uses skills in formal specification, understanding of app behaviour (by studying open-source apps), possibly leading to prototyping a software tool to perform run-time checking that the claimed restrictions are adhered to. Suitable for good 3rd or 4th year undergraduates, or MSc, Concurrency, Concurrent Programming, Computer Security all possibly an advantage. Other projects within this domain possible, according to interest and inspiration.

Prerequisites:

Concurrency, Concurrent Programming, Computer Security all possibly an advantage.

(joint with Michael Goldsmith)

Technology-layer social networks: investigate the potential to identify relationships between people via technology metadata - which machines their machines are "friendly" with. Research will involve identification of all metadata available from the network layer, app layers and the data layer, development of appropriate relationship models, and practical experimentation / forensic-style work exploring how to extract relationships between technologies and identities. Appropriate for 4th year undergraduates or MSc.

LogMap is a highly optimised ontology matching system developed by members of the Knowledge Representation and Reasoning Group with EPSRC funding (see http://www.cs.ox.ac.uk/projects/LogMap/index.html for details). The NCBO Bioportal (http://bioportal.bioontology.org) is a large repository of bio-medical ontologies and cross-references between them. The goal of this project is to exploit the information provided by BioPortal as background knowledge to improve ontology matching results in LogMap. Main tasks associated to the project: - Understanding how other matching tools (such as AgrMaker and GOMMA) exploit BioPortal to improve their results. - Understanding communication with Bioportal web services to query ontologies, mappings and other resources. - Understanding the LogMap's algorithm and devising a suitable way to communicate with BioPortal without harming scalability. - Implementing BioPortal access in LogMap. - Comparison with other matching tools.

LogMap is a highly optimised ontology matching system developed by members of the Knowledge Representation and Reasoning Group with EPSRC funding (see http://www.cs.ox.ac.uk/projects/LogMap/index.html for details). In applications requiring very accurate mappings, user intervention during the matching process becomes essential. LogMap implements basic features allowing domain experts to interactively contribute to the matching process. These features are, however,still rather rudimentary. The main goal of this project is to extend and improve LogMap's support for interactive ontology matching. From an algorithmic point of view, the main challenge is to limit to a minimum the number of questions that need to be asked to a human expert, while maximising the benefit of experts' feedback. From an application development point of view, the main goal is to develop a graphical front-end for LogMap that facilitates user interaction.

(Joint supervisior with G Orsi) Most of the information on commercial websites (e.g., Amazon, Rightmove, and Autotrader) is rep-resented by (semi-)structured pages where the interesting data is structured into de_ned structured or visual patterns. However, some critical information is often represented with an image or a chart. As an example, on many real-estate websites, data about the energy e_ciency of the property is represented by an EPC Chart (http://www.epcchart.com/), while the actual size of the rooms is represented through a oor-plan http://en.wikipedia.org/wiki/Floor_plan). Have you ever tried to search for an energy-e_cient property or one with a large bedroom? The answer is: you can't. This project is concerned with the study of semantic image analysis techniques that can be used to locate and extract interesting objects from pictures and charts on the web. The goal is to enhance current search technology with object-search capabilities for images, a _eld that o_ers challenging research and potential commercial opportunities. The project will be conducted within the DIADEM project (http://diadem.cs.ox.ac.uk). Good knowledge of Java is required, previous knowledge about image analysis, computer vision and OCR technology is preferred.

(Joint with G Grasso)

OXPath (http://diadem.cs.ox.ac.uk/OXPath/) is a wrapper language developed at Oxford in the DIADEM (diadem-project.info) project, extending standard XPath. It is particularly well suited for extraction from rich internet applications with sophisticated client-side interfaces, as well as to facilitate web automation and web crawling. OXPath has already been applied in several projects by researchers and practitioners, and it is available as a Java API (open source) interfacing with a real web browser. In this project we aim at providing a native Javascript implementation of OXPath. Nowadays Javascript has gained increasing interest and popularity thanks to the availability of prominent engines (e.g., Google V8 Javascript Engine http://code.google.com/p/ v8/) and open source frameworks (e.g, Node.js http://nodejs.org/), that allow highly scalable server-side Javascript execution. The outcome of this thesis is the implementation in Javascript of various fragments of OXPath characterized by increasing complexity. This will involve, for instance, the realization of a parser, and caching/memoization structures supporting the evaluation of OXPath. This MSC projects provides an opportunity to familiarize yourself with web frameworks and languages for data extraction such as XPath, OXPath, Javascript, and Node.js. Some knowledge of these languages would be desirable. Knowledge of Unix is highly recommended.

The wealth of information on the web is exceeding any other human-created source of information by orders of magnitude. Harnessing that data, however, requires increasingly automated methods that can collect relevant data from many websites and lter it,e .g., for further human consumption. OXPath (http://diadem.cs.ox.ac.uk/OXPath/) is a wrapper language developed at Oxford in the DIADEM (diadem-project.info) project. It is particularly well suited for extraction from rich internet applications with sophisticated client-side interfaces. Manually creating such wrappers, however, still remains a daunting task. In this project, we therefore aim to develop a method for learning OXPath wrappers from sets of annotated examples, that indicate, e.g., what data to extract or which actions to perform. The challenge in such a learning algorithm lies in the need to abstract from multiple examples to a single, compact OXPath expression that should be close to optimal under a set of additional criteria. Though there is a signi cant body of literature on learning XPath expressions, OXPath is a richer language and introduces new challenges. We also speci cally aim at extensive experimental validation of the developed techniques. This project is particularly suited for students interested in modern web technology and familiar with compiler design or query optimization. The learner will be implemented in Java, where we provide a set of customized APIs for action execution and DOM interaction.

(Supervisor G Grasso)

We want to develop an innovative on-line service to help users in their shopping: After specifying a shopping list of products, the system should identify the best shops to buy them from, ranked by di_erent criteria. For instance, the system might search for the least expensive supermarket or nearest grocery shop selling a set of products. The student will build upon the data extraction facilities available in DIADEM (diadem-project.info), in particular OXPath (http://diadem.cs.ox.ac.uk/OXPath/), a wrapper language facilitating web data extraction and automatizing web interactions. For this reason, this project requires a preliminary study of languages like XPath and OXPath and their semantics. The project outcome is a web portal with a modern layout, supporting at least user registration, shopping list speci_cation, and two optimization scenarios, such as best price and closest location (more features if time permits). Knowledge of Java is required, previous experiences in web development and databases are recommended.

(Joint with Sadie Creese) Kinect interface development for cybersecurity visual analytics tool: using the open development environment for Kinect, to develop an alternative HCI for the Oxford CyberVis tool http://www.cs.ox.ac.uk/projects/cybervis/ (focusing on navigation of the CyberVis environment). As CyberVIs is primarily developed in JAVA a good understanding that language is essential in order to interface Kinect to CyberVis. Suitable for 3rd or 4th year undergraduates, or MSc. Other projects on novel human-computer interfaces for security possible, depending on interest and inspiration.

(Joint with Sadie Creese) Smartphone security: one concrete idea is the development of a policy language to allow the authors of apps to describe their behaviour, designed to be precise about the expected access to peripherals and networks and the purpose thereof (data required and usage); uses skills in formal specification, understanding of app behaviour (by studying open-source apps), possibly leading to prototyping a software tool to perform run-time checking that the claimed restrictions are adhered to. Suitable for good 3rd or 4th year undergraduates, or MSc, Concurrency, Concurrent Programming, Computer Security all possibly an advantage. Other projects within this domain possible, according to interest and inspiration.

Prerequisites:

Concurrency, Concurrent Programming, Computer Security all possibly an advantage.

Background: The work will be done in the context of the large ERC project DIADEM: Domain-centric Intelligent Automated Data Extraction Methodology whose goal is to automate web data extraction in specific application domains such as real estate, restaurants, and so on.

Principal goal of the MSc or Honour School project:

This project consists in a case-study on web automation tasks in order to validate the ease-of-use of existing tools of web automation such as OXPath and ChickenFoot.
In particular, given some (complex) real tasks on the web, we want to study how straighforward would be solving them by using such tools.
This proposal could lead to a survey on existing web automation tools, as well as for improving the usability of OXPath.

Skills Needed: This project requires good analytic and theoretical skills. Also, knowledge of XPath and Java is preferred.

Supervision: This project will be co-supervised by Dr. Tim Furche

Background: There are several projects available. The work will be done in the context of the large ERC project DIADEM: Domain-centric Intelligent Automated Data Extraction Methodology whose goal is to automate web data extraction in specific application domains such as real estate, restaurants, and so on. Ultimately, we want to construct a system that is able to automatically navigate Web pages within a given application domain and extract relevant data from that pages. For example a system for the real-estate domain should accept as input an URL of an estate agent and output all properties (houses or flats) that are currently advertised by this agent to be for sale. The output should be a highly structured XML file obeying a certain pre-defined schema. 

Principal goal of the MSc or Honour School project: Contribute to the DIADEM project by providing useful studies and building blocks. Examples of such studies or building blocks are:

• A characterization of typical patterns on web pages of a certain application domain.
• A characterisation of access patterns for search masks and navigation sequences on web pages belonging to specific domains.
• Software for the automatic construction of dictionaries of domain-specific terms extracted from Web pages.
• Software for identifying compound data objects on domain-specific web pages.
• Implementation of building blocks of a reasoner over web data objects.
• Selection and integration of existing annotators for Web page analysis.
• Definition of new annotators.
• Implementation of a scheduler for highly parallel web data extraction through cloud computing.
• Testing components of the DIADEM system.

Note: The DIADEM project runs from 2010 to 1015. Every year only a few MSc or Honour School projects will be available. Some will be co-supervised by DIADEM research staff.

Skills Needed: Each of these projects requires good analytic and theoretical skills, software engineering skills, knowledge of web programming and web data processing, good knowledge of Java and Eclipse.

Background: The work will be done in the context of the large ERC project DIADEM: Domain-centric Intelligent Automated Data Extraction Methodology whose goal is to automate web data extraction in specific application domains such as real estate, restaurants, and so on.

Principal goal of the MSc or Honour School project:

A relevant task in Deep Web data extraction system is the so-called Form-Probing. Roughly, given a web form where each field is annotated with some concept, probing a form involves tasks such as:
(i) validating its annotations by submitting and checking the response page, (ii) forming meaningful queries given a database of values to submit, (iii) devise smart approaches to reduce the number of possible queries (e.g. in case of fields dependent on each other, like Min and Max price).
This proposal aims at designing probing heuristics and developing  such techniques in an extensible framework (plug-in).

Skills Needed: This project requires good theoretical, analytic and software engineering skills. Knowledge of Java and web-technologies is also required.

Supervision: This project will be co-supervised by Dr. Tim Furche.

Bioinformatics Projects can be found here.

If you choose any of these projects you must find a joint supervisor from the Computing Laboratory. Pete Jeavons can advise on a suitable choice.

This is a compiler project, also requiring familiarity with concurrency.

The parallel programming language occam is essentially an implementable sublanguage of CSP. The aim of this project is to produce a small portable implementation of a subset of occam; the proposed technique is to implement a virtual machine based on the inmos transputer, and a compiler which targets that language.

One of the aims of the project is to implement an extension to occam which permits recursion; more ambitious projects might implement a distributed implementation with several communicating copies of the virtual machine. Other possibilities are to produce separate virtual machines, optimised for displaying a simulation, or for efficiency of implementation, or translating the virtual machine code into native code for a real machine.

This is an interactive programming project with some logic simulation behind it.

The idea is to produce a simulator for a traditional logic breadboard. The user should be able to construct a logic circuit by drawing components from a library of standard gates and latches and so on, and connecting them together in allowable ways. It should then be possible to simulate the behaviour of the circuit, to control its inputs in various ways, and to display its outputs and the values of internal signals in various ways.

The simulator should be able to enforce design rules (such as those about not connecting standard outputs together, or limiting fan-out) but should also cope with partially completed circuits; it might be able to implement circuits described in terms of replicated sub-circuits; it should also be able to some sort of standard netlist.

It might be that this would make a project for two undergraduates: one implementing the interface, the other implementing a simulator that runs the logic.

This is an interactive graphics programming project.

This is an idea based on a child's toy, consisting of a collection of acrylic pieces. There are several colours, and two shapes: isosceles right-angled triangles, and rhombuses with 45 degree and 135 degree angles and sides to match the equal sides of the triangles. The player arranges (all) the pieces in one of the many ways that produce a square of the right size, with a pattern that has several (reflectional or rotational) symmetries.

The project is to design and build a small program that can be used to simulate the play: perhaps the user specifies symmetries, and then places a single piece which is replicated in several places as required by the symmetry.

There is a small subtlety in that the target square has a side which is an irrational number of the unit length (edge of the rhombus), so there is no integer grid on whcih the pieces lie. (It is very easy to make a mistake with the real toy which almost produces a square of the wrong size.)

The aim is to take some mathematics that would be within the grasp of a mathematically-inclined sixth-former and turn it into some attention-grabbing web pages. Ideally this reveals a connection with computing science. I imagine that this project necessarily involves some sort of animation, and I have visions of Open University television maths lectures.

The programming need not be the most important part of this project, though, because some of the work is in choosing a topic and designing problems and puzzles and the like around it. There's a lot of this sort of thing about, though, so it would be necessary to be a bit original.

Think of GeomLab (and then perhaps think of something a little less ambitious). It might involve logic and proof, it might be about sequences and series, it might be about graphs, it might be about the mathematics of cryptography... you might have something else in mind.

Steganography means hiding a hidden payload within an apparently-innocent cover, usually an item of digital media. Facebook is the ideal platform for the transmission of payload-carrying images, since images are so commonly uploaded and shared. And facebook does not permit encrypted communications between users, who might seek an alternative way to preserve their privacy. This project is to develop a steganography app for facebook, which allows messages to be sent and received inside pictures.

Prerequisites:

The only prerequisite is to understand how apps are developed on facebook. Be warned: the supervisor knows nothing of the facebook platform, and the student is largely on their own when it comes to the programming. The supervisor will simply give advice about what steganography functionality should be implemented.

Steganography means hiding a hidden payload within an apparently-innocent cover, usually an item of digital media. Steganalysis is the art of detecting that such hiding took place. The most effective ways to detect steganography are machine learning algorithms applied to "features" extracted from the media involved, trained on massive sets of known cover and stego objects. But, unlike in traditional machine learning, we can analyse (or simulate) the effect of embedding on features to a high level of detail. It turns out that some features are "equivalent" in that the same thing happens to them under embedding, in which case it is more efficient to combine them. This project is to formulate a proper definition of which features should be combined, and implement software to do so. The combined features can be benchmarked against the standard features using machine learning tools.

Prerequisites:

Discrete maths, linear algebra, machine learning

Steganography means hiding a hidden payload within an apparently-innocent cover, usually an item of digital media. There is lots of literature on hiding, and detection of hiding, in images, but rather little in audio. But mp3 audio is widely transmitted on file-sharing networks and thus provides an excellent cover. One slightly old-fashioned example of mp3 steganography can be found here http://www.petitcolas.net/fabien/steganography/mp3stego/. This project is to explore and develop mp3 steganography, adapting modern image hiding techniques to the audio format and implementing hiding and extraction programs.

Prerequisites:

No course prerequisites, but this project is only suitable for students who are already familiar with the details of mp3 format and encoding, for example those who have worked on open-source audio codecs. It is NOT possible to learn the format within the time available.

 Daniel Kroening is happy to supervise projects related to

• automated hardware and software verification
• program analysis
• SAT and decision procedures
• applications of SAT or SMT in other areas, e.g., systems biology or finance

For a list of sample projects, see here.

I am happy to supervise the following projects:

Model checking for DNA

Software verification for sensor networks

Model checking for automated negotiation protocols

Please contact Marta.Kwiatkowska@comlab.ox.ac.uk if you are interested

A security protocol consists of an exchange of messages between two or more agents, with goals such as establishing a cryptographic key, or authenticating the identities of the agents. These protocols are designed to operate in particularly hostile environments, where an adversary or intruder may be trying to attack the protocol, for example to learn the value of a key. Designing secure protocols has proven to be remarkably difficult; in some cases, attacks have been discovered several years after the protocol was first suggested. We have developed a systematic technique for analysing these protocols. Briefly the technique is as follows:

• The protocol is described formally in an abstract language.
• A compiler called Casper is used to compile the protocol description into a description in the process algebra CSP.
• The CSP description is fed to the model checker FDR, which tests whether the protocol correctly achieves its goals. In the case where the system does not meet a goal, FDR returns a sequence of messages that demonstrates how the goal fails, which is equivalent to the sequence of steps the intruder must take in order to attack the protocol.

A recent extension of these ideas has been to the analysis of layered protocols, where a special-purpose, application-specific protocol is layered
on top of a general-purpose secure transport layer protocol, such as SSL/TLS.
For such layered architectures, the CSP model created by Casper abstracts away from the details of the secure transport protocol, and just models the
security services it provides to the application protocol [3].  The goal of  this project would be to apply this technique to study one or more layered
protocols.  An alternative would be to apply these techniques to so-called human-mediated protocols [4], where a human is responsible for transferring or
verifying some messages in the protocol; we believe that similar analysis techniques can be applied to such protocols.

Prerequisites:

The Concurrency and Computer Security courses would be prerequisites for this project.

References

• [1] Gavin Lowe, Casper: A Compiler for the Analysis of Security Protocols, Journal of Computer Security, 1998.
• [2] Peter Ryan, Steve Schneider, Michael Goldsmith, Gavin Lowe, Bill Roscoe, Modelling and Analysis of Security Protocols, Addison Wesley, 2001.
• [3] Specifying Secure Transport Layers, Christopher Dilloway, Gavin Lowe.  In 21st IEEE Computer Security Foundations Symposium (CSF 21) 2008.
  http://web.comlab.ox.ac.uk//files/116/channels.pdf.
• [4] Exploiting Empirical Engagement in Authentication Protocol Design, Sadie Creese, Michael Goldsmith, Richard Harrison, Bill Roscoe, Paul Whittaker, and
  Irfan Zakiuddin.  In Proceedings of SPPC 2005, ttp://web.comlab.ox.ac.uk/people/Bill.Roscoe/publications/103.pdf

The aim of this project would be to build a compiler (or compiler plug-in) to translate Scala code written using the CSO library into corresponding CSP models. It would also be useful to develop techniques for automating analysis of various desirable properties, such as freedom from race conditions, and to develop techniques for abstracting some aspects of the CSP models so as to make model checking feasible.

Prerequisites:

The Concurrency, Concurrent Programming and Compilers courses would be prerequisites.

(Joint supervision with Tom Gibson-Robinson)

Probe [1] is a tool that allows CSP [2] processes to be visualised and manually explored. The goal of this project would be to build a new version of Probe that is significantly more user-friendly whilst supporting additional debug functionality and alternative display formats. This would be built on top of the libcspm Haskell library [3] that provides a parser, typechecker and evaluator for machine CSP. Prerequisites for this would be strong functional programming skills (e.g. via the Functional Programming course) and a good understand of CSP (e.g. via the Concurrency course).

Prerequisites:

Prerequisites for this would be strong functional programming skills
(e.g. via the Functional Programming course) and a good understand
of CSP (e.g. via the Concurrency course).

References:

[1] Probe, Formal Systems, http://www.fsel.com/.
[2] Understanding Concurrent Systems, Bill Roscoe.
[3] libcspm, Thomas Gibson-Robinson, https://github.com/tomgr/libcspm.

CSO [1] is a concurrency and communication library for the Scala programming language. The aim of this project would be to extend CSO with channels that allow secure communication between processes. The channels should implement some of the specifications in [2]. The Concurrent Programming and Computer Security courses would be prerequisites.

Prerequisites:

The Concurrent Programming and Computer Security courses would be prerequisites.

References:

• [1] Communicating Scala Objects, Bernard Sufrin. In Communicating Process Architectures, 2008. http://users.comlab.ox.ac.uk/bernard.sufrin/CSO/cpa2008-cso.pdf.

• [2] Specifying Secure Transport Layers, Christopher Dilloway, Gavin Lowe. In 21st IEEE Computer Security Foundations Symposium (CSF 21) 2008. http://web.comlab.ox.ac.uk//files/116/channels.pdf.

Background:

The next revolution in Web search as one of the key technologies of the Web has just started with the incorporation of ideas from the Semantic Web, aiming at transforming current Web search into some form of semantic search and query answering. Next-generation technologies for semantic search and query answering on the Web can be realized via knowledge bases extracted from the Web relative to an underlying ontology. The realization of such knowledge bases requires a principled and sensible way of managing conflicting information. Though inconsistency has been addressed for many years now in artificial intelligence and database theory, the search for flexible and computationally efficient inconsistency-tolerant semantics is a very active research topic.

Potential Projects:

● Characterization of inconsistency and repairing for different fragments of the Datalog+/-family of ontology languages.

● Study of desirable properties of repairs and development of adequate preference relations among repairs.

● Development of alternative inconsistency-tolerant semantics for query answering in different fragments of Datalog+/-: analysis of the trade-off between quality of answers and computation cost.

● Argumentation is one of the most well-known and capable systems for inconsistency management. The study of argumentation aspects and frameworks for different fragments of the Datalog+/- family of ontology languages as part of the above points.

● Implementation of repairing and inconsistency-tolerant query answering techniques on fragments and extensions of Datalog+/-.

Prerequisites:

Participation in all aspects of the project require good analytical skills and background in knowledge representation and reasoning (in particular, first-order logic and logic programming). For the theoretical aspects, background in computational complexity and database theory would be ideal. The practical (implementation-oriented) parts require software engineering skills, knowledge of web programming to develop web interfaces, as well as good knowledge of Java and Eclipse.

Supervision:

The projects based on implementation will be supervised by Maria Vanina Martinez, while the ones based on theoretical aspects will be co-supervised by Thomas Lukasiewicz and Maria Vanina Martinez.

Background:

The next revolution in Web search as one of the key technologies of the Web has just started with the incorporation of ideas from the Semantic Web, aiming at transforming current Web search into some form of semantic search and query answering. Next-generation technologies for semantic search and query answering on the Web can be realized via knowledge bases extracted from the Web relative to an underlying ontology. Such knowledge bases require probabilistic data models, along with scalable query answering algorithms, which are both still major unsolved problems. They may be based on integrating (i) ontology languages, (ii) database technologies, and (iii) formalisms for managing probabilistic uncertainty.

Potential Projects: 

● Characterization of ranking for non-probabilistic ontologies via explicitly defined user preferences. Key questions involve how to represent the user preferences, how to automatically obtain them (e.g., from the Web), and how to use them for ranking answers to ontological queries over knowledge bases.

● Extension of the above ranking techniques to probabilistic ontologies, i.e., combining the relevance of an answer with the probability that it is in fact true.

● Characterization of top-k query answering based on user preferences, and extension to probabilistic ontologies.

● Implementation of ranking and top-k querying on fragments of probabilistic Datalog+/-.

● Adaptation of sampling techniques for efficient query answering in probabilistic ontologies.

● Experimental evaluation of implementations over both synthetic and real-world data.

Prerequisites:

Participation in all aspects of the project require good analytical skills, and background in knowledge representation and reasoning (in particular, first-order logic and logic programming). For the theoretical aspects, background in computational complexity and database theory would be ideal. The practical (implementation-oriented) parts require software engineering skills, knowledge of Web programming to develop Web interfaces, as well as good knowledge of Java and Eclipse.

Supervision:

The projects based on implementation will be supervised by Gerardo Simari, while the ones based on theoretical aspects will be co-supervised by Thomas Lukasiewicz and Gerardo Simari.

Many experts predict that the next huge step forward in Web information technology will be achieved by adding semantics to Web data, and will possibly consist of (some form of) the Semantic Web. The project is based on a novel approach to Semantic Web search, called Serene, which allows for a semantic processing of Web search queries, and for evaluating complex Web search queries that involve reasoning over the Web. The goal of the project is to develop a Semantic Web search system on top of Serene for a collection of Web pages relative to an underlying ontology.   

The Sansone Group at the Oxford e-Research Centre offers several student projects throughout the year, focused on developing and applying new methods and tools for improving management, curation and sharing of data in life science.

Supervisors: Susanna-Assunta Sansone; Philippe Rocca-Serra and Eamonn Maguire.

Information about this project can be found at: http://www.oerc.ox.ac.uk/research/sansone/projects/student-projects#ontology-acquisition

The Sansone Group at the Oxford e-Research Centre offers several student projects throughout the year, focused on developing and applying new methods and tools for improving management, curation and sharing of data in life science.

Supervisors: Susanna-Assunta Sansone; Philippe Rocca-Serra and Eamonn Maguire.

Information about this project can be found at: http://www.oerc.ox.ac.uk/research/sansone/projects/student-projects#graph

(Joint Supervisor with Ian Horrocks)

The Sansone Group at the Oxford e-Research Centre offers several student projects throughout the year, focused on developing and applying new methods and tools for improving management, curation and sharing of data in life science.

Supervisors: Susanna-Assunta Sansone; Philippe Rocca-Serra and Eamonn Maguire.

Information about this project can be found at: http://www.oerc.ox.ac.uk/research/sansone/projects/student-projects#validation

Commercial use of the Internet is becoming more and more common, with an increasing variety of goods becoming available for purchase over the Net. Clearly, we want such purchases to be carried out securely: a customer wants to be sure of what (s)he's buying and the price (s)he's paying; the merchant wants to be sure of receiving payment; both sides want to end up with evidence of the transaction, in case the other side denies it took place; the act of purchase should not leak secrets, such as credit card details, to an eavesdropper.

The aim of this project is to find out more about the protocols that are used for electronic commerce, and to implement a simple e-commerce protocol. In more detail:

Understand the requirements of e-commerce protocols;

Specify an e-commerce protocol, both in terms of its functional and security requirements;

• Understand cryptographic techniques;
• Understand how these cryptographic techniques can be combined together to create a secure protocol - and understand the weaknesses that allow some protocols to be attacked;
• Design a protocol to meet the requirements identified;
• Implement the protocol.

A variant of this project would be to implement a protocol for voting on the web (which would have a different set of security properties).

Prerequisites for this project include good program design and implementation skills, including some experience of object-oriented programming, and a willingness to learn about protocols and cryptography. The courses on concurrency and distributed systems provide useful background for this project.

1 Jonathan Knudsen, Java Cryptography, O'Reilly, 1998.

Please see Dr Dan Olteanu's web page (http://www.cs.ox.ac.uk/people/dan.olteanu.html) for further details

More details can be found at (http://www.cs.ox.ac.uk/people/dan.olteanu.html) and Dr Olteanu would be happy to discuss specific projects within the aforementioned topics with interested students.

Please see Dr Dan Olteanu's web page (http://www.cs.ox.ac.uk/people/dan.olteanu.html) for further details

More details can be found at (http://www.cs.ox.ac.uk/people/dan.olteanu.html) and Dr Olteanu would be happy to discuss specific projects within the aforementioned topics with interested students.

Today, uncertainty is commonplace in data management scenarios dealing with data integration, sensor readings, information extraction from unstructured sources, or whenever information is manually entered and is therefore prone to inaccuracy or partiality. In these scenarios, uncertainty arises from the existence of alternatives for mapping schemas of different sources or for possible non-identical record duplicates, different interpretations of sensor data, multiple extraction possibilities from unstructured data, or several possible readings of manually filled forms respectively.

To accommodate uncertainty, the current data management technology should pursue a paradigm shift from deterministic to possible worlds semantics and address the basic data management problems in the new context. Projects on this topic should offer support for this paradigm shift by investigating some of the following directions

• compact representation systems for large sets of possible worlds,
• techniques for processing and constraints on succinct representations of possible worlds,
• uncertainty-aware query languages beyond relational algebra.

All aforementioned directions can lead to both theoretical and practical (implementation-oriented) projects. Anyone interested in doing a project in one of these topics is encouraged to get in touch with Dan Olteanu to explore specific ideas, such as

• Query Evaluation: Tractability and Efficient Algorithms
• Approximate and incremental view maintenance in probabilistic databases
• Synthesising query mappings for input and output probabilistic data
• View materialization for query optimization in probabilistic databases
• Modelling and processing streams of uncertain sensor data
• Algebraic optimizations for the MayBMS query language

Prerequisites: All projects within this framework require prior exposure to databases, though some projects may only require knowledge of either database theory or database systems. In the latter case, strong C/C++ skills are essential (Proficiency in any other general-purpose programming language is in any case an important start). Students with very good marks in the Database Systems Implementation course are preferred.

Suggested reading

• Latest publications on SPROUT and MayBMS.
• Lyublena Antova and Christoph Koch and Dan Olteanu. From Complete to Incomplete Information and Back. SIGMOD 2007.
• Lyublena Antova and Thomas Jansen and Christoph Koch and Dan Olteanu. Fast and Simple Relational Processing of Uncertain Data. ICDE 2008.
• Nilesh Dalvi and Dan Suciu. Efficient query evaluation on probabilistic databases. VLDB 2004.

Model checking has emerged as a powerful method for the formal verification of programs. Temporal logics such as CTL (computational tree logic) and CTL* are widely used to specify programs because they are expressive and easy to understand. Given an abstract model of a program, a model checker (which typically implements the acceptance problem for a class of automata) verifies whether the model meets a given specification. A conceptually attractive method for solving the model checking problem is by reducing it to the solution of (a suitable subclass of) parity games. These are a type of two player infinite game played on a finite graph. The project concerns the connexions between the temporal logics CTL and / or CTL*, automata, and games. Some of the following directions may be explored. 1. Representing CTL / CTL* as classes of alternating tree automata. 2. Inter-translation between CTL / CTL* and classes of alternating tree automata 3. Using B¨uchi games and other subclasses of parity games to analyse the CTL / CTL* model checking problem 4. Efficient implementation of model checking algorithms 5. Application of the model checker to higher-order model checking.

References:

Orna Kupferman, Moshe Y. Vardi, Pierre Wolper: An automata-theoretic approach to branchingtime model checking. J. ACM 47(2): 312-360 (2000).
http://dx.doi.org/10.1145/333979.333987

Rachel Bailey: A Comparative Study of Alorithmics for Solving B¨uchi Games. University of Oxford MSc Dissertation, 2010.
http://www.cs.ox.ac.uk/people/luke.ong/personal/publications/RachelBailey_MScdissertation.pdf

Dr. Vasile Palade (vasile.palade@cs.ox.ac.uk) is willing to supervise MSc projects in machine learning, ranging from more theoretical approaches to practical applications of machine learning. A preference will be given for projects on neural networks, support vector machines, evolutionary computation and fuzzy techniques applications to problems from the Bioinfomatics area, web usage mining, financial modeling, but other options will be considered too (e.g., character and image recognition). Please feel free to contact him and discuss about possible projects in these areas.

Pre-requisites: Computer graphics, Object-oriented programming

The idea behind this project is to build an educational tool which enables the stages of the graphics pipeline to be visualised. One might imagine the pipeline being represented by a sequence of windows; the user is able to manipulate a model in the first window and watch the progress of her modifications in the subsequent windows. Alternatively, the pipeline might be represented by an annotated slider widget; the user inputs a model and then she moves the slider down the pipeline, watching an animation of the process

Sentences like: `John likes Chopin, but Mary doesn't', or `John likes films, but not plays' contain ellipsis - `missing' components that have to be filled in from earlier parts of the sentence: John likes Chopin, but Mary doesn't like Chopin', `John likes films, but John doesn't like plays'. If you run the first pair of sentences through a parser like the Stanford parser:

(http://nlp.stanford.edu:8080/parser/index.jsp) you will see that it gets the constituent structure right, but doesn't attempt to capture the interpretation (see the dependency representations for semantically relevant information).

This project will attempt to develop and test a post-processing module for the Stanford parser which will interpret some common cases of ellipsis.

Prerequisites: some familiarity with linguistic theories of ellipsis.

A collaborator at Google has developed a logical language aimed at representing some aspects of the meaning of sentences in a linguistically motivated way, derivable from a dependency parse. You can read about it here: http://aclweb.org/anthology-new/W/W11/W11-0103.pdf

While the logic can be given a denotational semantics, it has yet to be provided with a proof theory in order that inferences can be drawn from sentences translated into it. This project aims to develop a proof theory for at least part of this logic, and if possible, test it via an implementation.

Prerequisites: only suitable for someone who has done BOTH the Computational Linguistics AND the Knowledge Representation and Reasoning courses.

Timed CSP reinterprets the CSP language in a real-time setting and has a semantics in which the exact times of events are recorded as well as their order. Originally devised in the 1980s, it has only just been implemented as an alternative mode for FDR. The objective of this project is to take one or more examples of timed concurrent system from the literature, implement them in Timed CSP, and where possible compare the performance of these models with similar examples running on other analysis tools such as Uppaal.

References:

(Reference Understanding Concurrent Systems, especially Chapter 15, and Model Checking Timed CSP, from AWR's web list of publications)

Jointly supervised by Stephen Pulman and Mehrnoosh Sadzradeh.

A background of Computational Linguistics is required

Pre-group grammars are a recent grammatical formalism somewhat similar to categorial grammar. The formalism is of interest to computational linguistics because it can be assimilated to category theory, computer scientists' favourite theoretical formalism. This project is to develop a parser for pre-group grammars, and, time permitting, investigate probabilistic disambiguation for the formalism. A paper describing the formalism is at: ftp://ftp.math.mcgill.ca/pub/lambek/natlangproc.pdf

Use Keiko to implement a simple language that is purely object-oriented. Study the compromises that must be made to get reasonable performance, comparing your implementation with Smalltalk, Ruby or Scala.

Please see http://spivey.oriel.ox.ac.uk/corner/Undergraduate_and_M.Sc._projects for further details.

The existing JIT for Keiko is very simple-minded, and does little more than translate each bytecode into the corresponding machine code. Either improve the translation by using one of the many JIT libraries now available, or adjust the Oberon compiler and the specification of the bytecode machine to free it of restrictive assumptions and produce a better pure-JIT implementation.

Please see http://spivey.oriel.ox.ac.uk/corner/Undergraduate_and_M.Sc._projects for further details.

At present, GeomLab programs show a performance that competes favourably with Python, making it possible to address tasks like computing images of the Mandelbrot set using a purely functional program that calls a function once for each pixel. But there is still a gap between the performance of GeomLab programs and similar ones written in Java or C, and more ambitious image-processing tasks would be made possible by better performance, particularly in the area of arithmetic. Explore ways of improving performance, perhaps including the possibility of improving the performance of GeomLab by allowing numbers to be passed around without wrapping them in heap-allocated objects, or the possibility of compiling the code for Haskell-style pattern matching in a better way.

Please see http://spivey.oriel.ox.ac.uk/corner/Undergraduate_and_M.Sc._projects for further details.

The Oberon compiler inserts code into every array access and every pointer dereference to check for runtime errors, like a subscript that is out of bounds or a pointer that is null. In many cases, it is possible to eliminate the checks because it is possible to determine from the program that no error can occur. For example, an array access inside a FOR loop may be safe given the bounds of the loop, and several uses of the same pointer in successive statements may be able to share one check that the pointer is non-null. Modify the Oberon compiler (or a simpler one taken from the Compilers labs) so that it represents the checks explicitly in its IR, and introduce a pass that removes unnecessary checks, so speeding up the code without compromising safety.

Please see http://spivey.oriel.ox.ac.uk/corner/Undergraduate_and_M.Sc._projects for further details.

GeomLab has a turtle graphics feature, but the pictures are drawn only on the screen. It should be possible to make a turtle out of Lego Mindstorms, then control it with an instance of Geomlab running on a host computer, with communication over Bluetooth.

Please see http://spivey.oriel.ox.ac.uk/corner/Undergraduate_and_M.Sc._projects for further details.

Produce an implementation of GeomLab's GUI and graphics library that works on the Android platform. Either use an interpreter for GeomLab's intermediate code to execute GeomLab programs, or investigate dynamic translation of the intermediate code into code for Android's virtual machine Dalvik.

Please see http://spivey.oriel.ox.ac.uk/corner/Undergraduate_and_M.Sc._projects for further details.

At present, Keiko supports only conventional Pascal-like language implementations that store activation records on a stack. Experiment with an implementation where activation records are heap-allocated (and therefore recovered by a garbage collector), procedures are genuinely first-class citizens that can be returned as results in addition to being passed as arguments, and tail recursion is optimised seamlessly.

Please see http://spivey.oriel.ox.ac.uk/corner/Undergraduate_and_M.Sc._projects for further details.

Alternative firmware for the Mindstorms robot controller provides an implementation of the JVM, allowing Java programs to run on the controller, subject to some restrictions. Using this firmware as a guide, produce an interpreter for a suitable bytecode, perhaps some variant of Keiko, allowing Oberon or another robot language of your own design to run on the controller. Aim to support the buttons and display at first, and perhaps add control of the motors and sensors later.

Please see http://spivey.oriel.ox.ac.uk/corner/Undergraduate_and_M.Sc._projects for further details.

The GeomLab language is untyped, leading to errors when expressions are evaluated that would be better caught at an earlier stage. Most GeomLab programs, however, follow relatively simple typing rules. The aim in this project is to write a polymorphic type checker for GeomLab and integrate it into the GeomLab system, which is implemented in Java. A simple implementation of the type-checker would wait until an expression is about to be evaluated, and type-check the whole program at that point. As an extension of the project, you could investigate whether it is possible to type-check function definitions one at a time, even when some of the functions they call have not yet been defined.

Please see http://spivey.oriel.ox.ac.uk/corner/Undergraduate_and_M.Sc._projects for further details.

The interval program analysis is a well-known algorithm for estimating the behaviour of programs without actually running them. The algorithm takes an imperative program, and returns, at each program point, interval constraints for variables in the program, such as 1 <= x <= 3 && 2 <= y. This algorithm assumes that all the functions called by the input program are defined in the program, so that the source code of every called function can be found in the program. However, in practice, this assumption is not necessarily met. Programs often use library functions whose source code is not available. The goal of this project is to lift this assumption. During the project, a student will develop an interval-analysis algorithm that works in the presence of calls to unknown library functions, implement the algorithm, and evaluate the algorithm experimentally.

Prerequisites:

A prerequisite of this project is the Compiler course.

Developing efficient concurrent data structures is nontrivial, and requires several interesting new programming techniques. In the context of shared-variable concurrency, researchers developed such data structures, often called nonblocking algorithms, which avoid using locks (expressed by the synchronized keyword in Java) and perform well even when many threads attempt to use the data structures at the same time. The goal of this project is to revisit these data structures designed for shared-variable concurrency, especially those found in Herlihy and Shavit's book "The art of multiprocessor programming", and to build corresponding data structures based on asynchronous message-passing passing or Actor model, which is supported by Erlang or Scala. The built data structures will be analysed theoretically (by proving their linearizability) or empirically (by measuring their performance) or both.

Prerequisites:

Although it is not required, it is desirable that a student carrying out this project took the Concurrent Programming course before.