Summer Students Projects in CAS
Several faculty members in the Department of Computing and Software are offering Summer positions in 2011. Please note, the eligibility criteria is: B- average and Canadian or Permanent Resident status.Hours of work and pay rates will vary by project.
Please apply to the supervisor as listed below. (The e-mail addresses are on the contact page.)
Connections between Primal-Dual and Iterative Rounding for designing approximation algorithms
Supervisor: Dr. George KarakostasDuring the past two decades, the primal-dual scheme has been a major tool for the design of algorithms with very good approximation factors for NP-hard problems. This method is based on the duality theorems of Linear Programming (LP): Strong duality ensures that satisfaction of complementary slackness conditions implies optimality of a (fractional) solution. "Good" relaxation (i.e., relaxation by a small factor) of these conditions can be shown to imply a good integral solution for the original problem formulated as an LP. The primal-dual method is based on the connection between a primal LP and its dual, but in recent years a new method called iterated rounding has been applied to a variety of problems, for which no equally good primal- dual schemes were known. Iterated rounding deals only with the primal LP formulation of the hard (say, minimization) problem, and very carefully rounds up a fractional solution piece-by-piece to an integral one. So, iterated rounding is a combinatorial primal method (like Simplex is a combinatorial method for solving LPs) and the primal-dual scheme involves both the primal and the dual (like similar methods for solving LPs). The aim of this project will be to explore the possible connections between iterated rounding and primal-dual schemes. We will try to understand their application to network design problems, and through that we will try to understand why each works so well on its own set of problems, and see whether there could be a method of transforming iterated routing algorithms into primal-dual ones and vice-versa. The immediate goal for the research team (supervisor, intern and at least one graduate student) will be to improve the approximation factor of network design problems, but the more ambitious one will be the development of new algorithm design methodologies that will try to encompass both iterated rounding and primal-dual schemes.
Required qualifications:
- The student involved with this project will be expected to have (or acquire) a basic knowledge of Linear Programming, and computational complexity (complexity of algorithms, NP-completeness, reductions, etc.) A solid Linear Algebra background is also essential, as is a good grasp of discrete mathematics.
Student Grades and Other Metrics Database
Supervisor: Dr. Spencer SmithDesign, implement and test tools to assist with understanding student retention for Level 1 Engineering. In particular, we are interested in the continuing development of a tool to track and analyze student grades and other metrics for Eng 1 students. The tool will help with collecting data, anonymizing the data and building the infrastructure so that data collection can continue in future years. Besides student grades (assignment grades, midterm grades, final grades, lab grades, etc.), the data will include Avenue activity, survey responses, highschool grades, and classroom and lab attendance. Proper software engineering methodologies and tool use will be emphasized.
Required qualifications:
- Software development and programming skills.
Two students needed for Designing Interactive Documents For Mobile Devices using Domain Specific Languages
Supervisor: Dr. Christopher Anand
In this project, we would like to explore the application of Domain Specific Languages (DSLs) to content consumption and creation on heterogeneous devices (focussing on mobile devices) with work-flow rules. DSLs are custom (often very compact) computer languages which can express information and processes in a restricted domain. General-purpose languages can express arbitrary programs, but this flexibility has several drawbacks: It is possible to express more undesirable behaviours than desirable behaviours and it is impossible to reliably separate the two with automatic tools.
If, for example, a largely text document requires embedded architectural drawings whose complexity stretches the abilities of a target smartphone, then the current practice would require the text to be embedded in a custom smartphone application. Targeting a different smartphone would require a re-write of the application. If, in addition, the roles of different users need to be respected by limiting the types and order or content changes, then this would have to be coded into the application as well. Mixing the content, visualization code and workflow rules together in the application will make it hard to port the application to a new smartphone or other device, and make it hard to test because it is too difficult to enumerate all the different ways user choices in the different user interface (UI) elements can interact. This is especially significant because the kind of automated testing which is routine on desktops, laptops and servers is not yet available (and may never be completely available) on smart phones and other mobile devices. While it is, in principle, possible to automate the testing of applications within desktop simulators, such simulators are not reliable enough, and probably will not be reliable enough for some time.
If, however, the different aspects: textual content markup, visualization widgets, and workflow rules could be captured by a formal DSL, an analysis similar to the analyses we have performed for multi-core parallel programs%
\footnote{{CK~Anand}, W~Kahl, An Optimized Cell BE Special Function Library Generated by Coconut, IEEE Trans. Computers, 58 (8) (2009) 1126--1138.}
would be able to automatically generate a minimal number of test scripts for manual testing, together with a proof that no UI errors are present. The key to making this work effectively is designing the DSL with the right level of abstraction and with the minimum amount and type of expressivity to be able to efficiently capture living documents in the target domain. Too much expressivity, and we lose the benefit of easy retargeting and test-case analysis. Too little expressivity, and we cannot do the work required.
To hear more about our previous work on DSLs, a good start is the Google Talk at the top of
this page
The goal of this project will be to examine one or more projects our industrial partner (Mississauga startup) is working on and formulate a DSL to capture documents in this project. To demonstrate the usefulness of these ideas, we will specify a subset of the language to be interpreted in a prototype application and analyzed for test completeness. The scope of the prototype will depend on the time it takes to formulate the DSL.
The language modelling will be in Haskell (haskell.org), but the main thing you need to know is how to specify languages using algebraic data types
(ref), and how mathematical induction works, so that you can reason in the following way: All trees can be built up from Leaves (single elements), and Pairs of Trees (the left and right branches), so if I know property P satisfies P(left) && P(right) => P(Branch left right), and P is true for Leaves, then P is true for all trees. An example of P for trees could be P(tree) = elements are sorted left <= right. An example of P we care about is
P(workflow) = updates to plumbing diagrams are only distributed after approval by a plumbing supervisor and supervising engineer.
The mobile device(s) we will target is not yet decided, but likely to be iPod Touches, since we already have some (and an iPad). In this case you will have to learn some Objective-C, and Cocoa frameworks.
Contact Christopher Anand
The dependently-typed programming language and proof checker Agda2 allows us to write functional programs that include their correctness proofs as part of the source code.
As part of an ongoing effort aiming to produce verified Agda implementations of general graph transformation mechanisms, this project will produce self-contained auxiliary libraries, in particular verified implementations of container data structures.
This project requires strength and interest in logics and discrete mathematics.
Agda
The dependently-typed programming language and proof checker Agda2 allows us to write functional programs that include their correctness proofs as part of the source code.
This project will be part of an ongoing effort aiming to produce verified Agda implementations of general graph transformation and also of more specific term graph transformation mechanisms that will be used in optimised machine code generation.
This project will produce verified implementations of selected transformation mechanisms, and expand the underlying theories as necessary.
This project requires strength and interest in logics and discrete mathematics.
Agda
The generic graph transformation, visualisation, and editing framework GraTraVis already supports programming of custom graph transformation mechanisms, and of custom visualisations in Cairo for 2D and in OpenGL for 3D graphical representation of graph models.
This project will add different new graph model instances to show off and improve these capabilities.
Candidates include:
Games are now played one devices of wildly varying size: from the wall-of-screens seen in ITB 225 to iPods and smartphones. Naturally, one cannot use the exact same game at all scales, but one can nevertheless be remarkably uniform - as witnessed say by Plants vs Zombies. Nevertheless, something things must change.
This project consists of two parts: 1. creating a "language of scale", which describes constraints associate to screen size, and 2. applying this language to component specialization. For this project, the focus will be on a single component: status display. As screen size varies, different real estate can be used for 'status display'; as screen real estate gets cramped, decisions must be made to restrict (and potentially eliminate) all permanent display of current status. The crux of the project is to understand what are the main decision factors involved, and to implement a prototype.
This project involves investigation of the design and implementation of safety critical systems for the nuclear industry using FPGA based platforms. The focus will be upon construction of pre-verified functional blocks that can be used to implement verifiably correct systems.
Required qualifications:
This project involves working with the Art Gallery of Hamilton (AGH) to develop an interactive application for the iPhone and/or Android based cellphones to help to promote the AGH. The student will have to work with AGH staff to develop the application content and implement it on a cellphone platform.
Required qualifications:
Verified Container Libraries in Agda
Supervisors: Dr. Wolfram Kahl
Verified Graph Transformation in Agda
Supervisor: Dr. Wolfram Kahl
Applications of 3D Graph Transformation in GraTraVis
Supervisor: Dr. Wolfram Kahl
GraTraVis is programmed in the
pure functional programming language
Haskell.
Scale and Games
Supervisor: Dr. Jacques Carette
FPGA Based Implementation of Verifiably Correct Safety Critical Systems
Supervisor: Dr. Mark Lawford
Interactive Musem App Development
Supervisor: Dr. Mark Lawford