MSc by Research - Student projects

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

Glass models are frequently used to model gene regulatory networks. A distinct feature of the Glass model is that its dynamics can be formalized as paths through multi-dimensional binary hypercubes. The goal of this project is to identify instances of Glass networks that are amenable to reasoning by an analysis of the binary codes that correspond to the hypercube paths. Specifically, we aim at exploring algorithmic methods for the synthesis of specific Glass networks based on these codes. This project is suitable both for very applied and for theoretical studies.

Model Checkers for concurrent programs have made tremendous progress in the past years. It's time to revisit the Linux Kernel with these methods, and investigate scalability and applicability of automated program analysis in this context. This is an applied project. 

Accurate timing analysis is crucial for obtaining the optimal clock frequency, and for other design stages such as power analysis. Most methods for estimating propagation delay identify multi-cycle paths (MCPs), which allow timing to be relaxed, but ignore the set of reachable states, achieving scalability at the cost of a severe lack of precision. Even simple circuits contain paths affecting timing that can only be detected if the set of reachable states is considered.

The goal of this project is to evaluate different methods for checking safety properties that identify MCPs. We plan to evaluate Craig Interpolation, Bounded Model Checking, and BDD-based Model Checking. 

Reasoning about the heap is one of the biggest challenges in program analysis. The goal of this project is to evaluate ways of combining Satisfiability Modulo Theories with a decision procedure for a fragment of Separation Logic.