projects
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
projects [2018/08/29 15:37] – lesperan | projects [2019/09/04 20:46] (current) – khatoll | ||
---|---|---|---|
Line 1: | Line 1: | ||
~~NOTOC~~ | ~~NOTOC~~ | ||
- | ====== Proposed Projects | + | ======Proposed Projects====== |
- | ====== Detecting and Visualizing anomalies in dynamic networks ====== | + | **Course**: EECS 4080 |
- | **Supervisor:** Aijun An | + | |
- | In this project, | + | **Project title:**\\ |
+ | A Survey on the State-of-the-Art Android Testing Tools and Techniques | ||
- | **Required | + | **Required |
+ | General CSE408x prerequisites | ||
- | **Recommended skills:** Experience with visualization tools is very helpful, Interest | + | **Project Description:**\\ |
+ | Compare to the traditional software applications, | ||
- | ====== Graphical User Interface for Power System Simulator ====== | + | **Proposed by:**\\ |
- | **Supervisor:** Afshin Rezaei | + | Franck VanBreugel, Song Wang and Zhen Ming (Jack) Jiang\\ |
- | The project is to develop a user-friendly Graphical User Interface (GUI) for a power system simulator program. Similar to all circuit simulation programs, the GUI should provide a library of the system components. These elements include not only the basic circuit elements such as resistor, capacitor, and inductor but also more complex equipment models such as transformers, | + | ---- |
- | **Required background: | ||
- | |||
- | ====== Development of a Standalone Power System Optimization Toolbox ====== | ||
- | **Supervisor: | ||
- | |||
- | Finding the optimum system condition and maximum/ | ||
- | In this project, the developer is expected to explore Intel FORTRAN Math Kernel Library (MKL) and Intel Mathematics and Statistics Library (IMSL) and develop a program code in FORTRAN to call built-in functions and perform the requested optimizations specified by the user. Due to compatibility of the MS Visual Studio with both FORTRAN and C++, some parts of the code can also be developed in C++. | ||
- | |||
- | **Required background: | ||
- | |||
- | |||
- | ====== Palpation Task Trainer ====== | ||
- | |||
- | **Supervisors: | ||
- | |||
- | Palpation of head and neck region is an integral part of a complete physical health assessment performed by both physicians (e.g., physician assistant; family doctor; Ear Nose and throat specialist and surgeon) and Nurses (Nurse practitioners, | ||
- | 1. Head to neck anatomical structure - Making the task trainer more " | ||
- | 2. Head and neck skin - Because we are focusing on palpation touching the skin and making the skin respond to touch is important. | ||
- | 3. Head to neck engaging and interactive - Several health care providers perform palpation. In fact there is a hierarchy among them (nurse vs doctor; family doctor vs Ear Nose and throat). Creating some kind of interactive game to find and characterize the gland with multidiscipline. | ||
- | |||
- | **Required Background: | ||
- | |||
- | **Other experience: | ||
- | |||
- | **Resources and readings:** Here are two links to articles we published. The reference list has more resources | ||
- | http:// | ||
- | http:// | ||
- | |||
- | |||
- | ====== Custom Camera App using the Andriod Camera 2 API ====== | ||
- | |||
- | |||
- | **Supervisor: | ||
- | |||
- | Cameras have a number of processing steps that convert the incoming sensor image to the final sRGB-JPEG image. | ||
- | |||
- | The primary goal of this project is to develop custom camera applications that manipulate individual components of the imaging pipeline (e.g., custom white-balance, | ||
- | |||
- | **Required Background: | ||
- | |||
- | |||
- | ====== Ultrasound simulation/ | ||
- | |||
- | **Supervisor: | ||
- | |||
- | Trans-esophageal echocardiography (TEE) is the standard of care for most cardiac surgeries and interventional cardiology procedures. It uses a thin and flexible ultrasound probe that is inserted down the esophagus in position beside the heart, and the echocardiographer adjusts the position and orientation of the probe from outside. For new clinicians, learning how to adjust the probe into the correct location for various views of the heart can be quite challenging. | ||
- | |||
- | The primary goal of this project is to develop an open source, inexpensive software simulation for training clinicians in the use of TEE ultrasound. Starting with a 3D-plus-time CT or MRI heart dataset, we will create simulated ultrasound images, and use a mouse to simulate the translation and rotation of the ultrasound probe. The software platform will render the simulated ultrasound, and provide the user with feedback on how well they can identify the standard TEE views. This project will involve a collaboration with clinicians in Toronto and London, Ontario. | ||
- | |||
- | **Required Background: | ||
- | |||
- | ====== 3D Fractal visualizations and Music ====== | ||
- | |||
- | |||
- | **Supervisor: | ||
- | |||
- | Visualizing and navigating through 3D fractals is very cool. Check out an example here: https:// | ||
- | |||
- | This project will investigate the connection between music and 3D fractal visualizations, | ||
- | |||
- | **Required Background: | ||
- | |||
- | |||
- | ====== Extracting Information from Music ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | While humans are quite good at extracting musical information from audio, such as tempo and time signature, computers have room for improvement in this regard. | ||
- | |||
- | This project will use the JUCE framework to create software that extracts such information from audio files. Existing algorithms will be implemented and compared, and possibly improved. The output will be both a stand-alone application, | ||
- | |||
- | **Required Background: | ||
- | |||
- | ====== Data-driven conceptual modeling within on-line communities ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | The wealth of data to be obtained from online communities is already well acknowledged. | ||
- | |||
- | **Required Background: | ||
- | |||
- | |||
- | ====== Proposed Project: Tangible Interactive Device Design and Evaluation, Assistive Technology ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | The objective of the ' | ||
- | This 4080 project will investigate the design, fabrication, | ||
- | |||
- | **Required Background: | ||
- | |||
- | |||
- | ====== Design and development of a low‐power backend PCB for brain neural signal processing and wireless data transmission ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | The student will be responsible for the design and testing of a printed circuit board (PCB) that receives brain electrophysiological signals from multiple recording sites; analyze, decode, and organizes them; and transmit them through a wireless link to a handheld (e.g., cellphone) or stationary (e.g. a laptop) device. The board must be designed while the strict power and area budgets of a medical device taken into account. | ||
- | Once developed, the prototype along with the currently‐available wearable brain monitoring device will form a complete wireless wearable solution for point‐of‐care brain monitoring and diagnosis applications. | ||
- | |||
- | **Required Background: | ||
- | |||
- | |||
- | ====== Distributed leader election for simple robots ====== | ||
- | |||
- | **Supervisors: | ||
- | |||
- | **Project: | ||
- | |||
- | To make this project more specific, and given the limited time available for an undergraduate student project, this project will explore certain properties of leader election algorithms, both with real and simulated groups of robots. Using a simulator, performance bottlenecks in the infection algorithm will be studied, considering cases where direct communication is limited to agents in the same local area. Simulations will be supported using a collection of real devices (Android devices) who can communicate with each other in the local environment using bluetooth and/or WIFI. If time permits, the project will also study possible enhancements of the infection algorithm as well as develop better upper bounds for the problem. | ||
- | |||
- | **Required skills:** knowledge of Java or Python. Interest in algorithms for a distributed collection of simple robot agents. Completion of 3rd year courses in computer science or computer engineering. | ||
- | |||
- | ====== Asynchronicity in infection algorithms ====== | ||
- | |||
- | **Supervisors: | ||
- | |||
- | **Project: | ||
- | |||
- | Infection algorithms are a class of algorithms within which individual agents exchange information via infection. That is, the algorithm proceeds by the various agents transmitting (infecting) each other with information. Under an assumption of synchronization — that is, a model in which no two agents can infect each other at precisely the same time — it is possible to derive models of expected time until all agents have been infected. But how does this algorithm adapt when agents can actually infect each other simultaneously? | ||
- | |||
- | **Required skills:** knowledge of Java or Python. Interest in algorithms for a distributed collection of simple robot agents. Completion of 3rd year courses in computer science or computer engineering. | ||
- | |||
- | ====== Simultaneous localization and mapping (SLAM) aided by a single unique directional landmark ====== | ||
- | |||
- | **Supervisors: | ||
- | |||
- | **Project: | ||
- | |||
- | SLAM algorithms have been developed for a large number of different environments, | ||
- | |||
- | **Required skills:** knowledge of Java or Python. Interest in algorithms for robots. Completion of 3rd year courses in computer science or computer engineering. | ||
- | |||
- | |||
- | ====== Immersive Virtual Worlds ====== | ||
- | |||
- | |||
- | **Supervisor: | ||
- | |||
- | We have a new and unique fully immersive virtual environment at York. The student would develop interactive 3D virtual worlds to study self motion perception and human computer interaction in a virtual world. In particular, working with a senior graduate student or postdoctoral fellow, the successful applicant would model 3D environments, | ||
- | |||
- | **Required Background: | ||
- | |||
- | |||
- | ====== Virtual Walking Devices ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | Simulating effective walking in an immersive virtual environment is challenging. Working with a senior graduate student, the successful applicant would help to develop a circular treadmill interface to support virtual walking metaphors. | ||
- | |||
- | **Required Background: | ||
- | |||
- | ====== Adapting a 3D Printer for Paste Extrusion ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | 3D printers are an enabling technology for engineering design. However most low- to medium-end printers can only extrude plastics through a hot-end extrusion system. A local company has developed a nozzle and pump system for pastes that can be integrated with existing printers. A student group is sought to design a mounting bracket for an existing TAZ 4 printer that can be used to augment its ABS extruder with a Discov3ry paste extruder. The bracket is to be printed with the TAZ and the design is to be released publicly to the open-source community. Sample prints, calibration routines and possible modifications to the printer' | ||
- | |||
- | **Required Background: | ||
- | |||
- | ====== Peer-to-Peer agent based applications in smart power grids ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | Multi-agent systems have been mentioned recently as a potential technology for several operational control objectives in smart power grids. The multi-agents technology allows the rapid and detailed creation of a system model and creates a robust framework for distributed control. The distributed control structure consists of components called control agents. These control agents try, through communication and negotiation with other control agents, to: 1) determine the current state of the system and/or subsystems and 2) make decisions (set their local actuators or communicate with other agents) in such a way that their own objectives are met as closely as possible and any constraints are satisfied. | ||
- | |||
- | This project aims to implement formulated distributed constraint optimization (DCOP) in a multi-agent platform for two objectives in smart grids: 1) voltage regulation and 2) electricity market,. There are several Java-based open source platforms for peer-to-peer agent based applications e.g. (JADE, Jadex, Jason, | ||
- | |||
- | The student should be a strong Java and MATLAB programmer. He should have prior knowledge about multi-agent platforms such as JADE. The work involves reading and understanding the formulated DCOP in smart grids and working with the supervisor and master/PhD student(s) to implement the developed algorithms and to measure the performance of the developed algorithm(s) in the multi-agent platform. | ||
- | |||
- | **Required Background: | ||
- | |||
- | |||
- | ====== Clustering High-Dimensional Data Sets ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | Clustering is a basic technique for analyzing data sets. Clustering is the process of grouping data points in a way that points within a group are more similar to each other than points in other clusters. Many clustering algorithms have been developed over the years. However no single algorithm works well for all data sets. Further, most clustering algorithms have running times of the order of n^2 or n^3, so that they are not feasible for data sets with hundreds of thousands of points. In this project we will design good clustering algorithms for large real data sets. In particular we are interested in Biological data sets. | ||
- | |||
- | Our data sets will include those obtained from Flow Cytometry data. Flow Cytometry is a common technique in many areas of Biology, particularly Immunology. Typical usage involves testing a blood sample for 25 attributes on a per-cell basis, and thus typical data sets are arrays of 500,000 points in a 25 dimensional space. The aim is to identify clusters that correspond to a biologist' | ||
- | |||
- | No Biology knowledge is required. The student should be a strong programmer. Knowledge of C/C++ is desirable but not essential. The work involves reading and understanding existing algorithms and working with the supervisor to design and implement improved algorithms and to measure the performance of the proposed algorithm(s). | ||
- | |||
- | For more information, | ||
- | |||
- | **Required Background: | ||
- | |||
- | |||
- | ====== Metaheuristic-based Optimization techniques ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | Optimization is a crucial step in many computational problems. For computational problems that seem (or are known to be) intractable, | ||
- | |||
- | The student should be a strong programmer. A good grasp of algorithms and knowledge of C/C++ are desirable but not essential. The work involves reading and understanding existing algorithms and working with the supervisor to design and implement improved algorithms and to measure the performance of the proposed algorithm(s). | ||
- | |||
- | **Required Background: | ||
- | |||
- | |||
- | ====== Genome-wide identification of plant micro RNAs ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | The Hudak Lab in the Biology Department has an opening for a fourth-year Honours student to assist with a bioinformatics project. We study the pokeweed plant, Phytolacca americana, which displays broad-spectrum virus resistance. To evaluate pokeweed gene expression, we recently sequenced the plant’s mRNA and small RNA transcriptomes under jasmonic acid (JA) treatment. JA is a plant hormone that mediates defence against pathogens and insect herbivores. We are interested in learning how pokeweed gene expression is regulated by miRNAs during biotic stress. Please note: no previous knowledge of biology is required. | ||
- | |||
- | For more information, | ||
- | |||
- | RNA sequencing- http:// | ||
- | |||
- | miRNAs- http:// | ||
- | |||
- | Working with the support of a PhD student, your project will involve: | ||
- | |||
- | - Prediction of micro RNA (miRNA) targets on the basis of complementary sequence matches | ||
- | - Correlation of miRNA and mRNA expression changes to identify genes that are regulated by miRNAs | ||
- | - Conducting pathway analysis to determine which biological processes are controlled by miRNAs | ||
- | - Construction of a miRNA/ | ||
- | |||
- | |||
- | **Requirements: | ||
- | |||
- | |||
- | ====== DDoS Attack using Google-bots ====== | ||
- | |||
- | |||
- | **Supervisor: | ||
- | |||
- | Not long ago, botnets - networks of compromised computers - were seen as the most effective (if not the only) means of conducting Distributed Denial of Service (DDoS) attacks. However, with the growing popularity and prevalence of application-layer over other types of DDoS attacks, the DDoS execution landscape is becoming increasingly more diverse. An especially interesting new trend is the execution of application-layer DDoS attacks by means of skillfully manipulated Web-crawlers, | ||
- | |||
- | **Recommended Background**: | ||
- | |||
- | |||
- | ====== Attentive Sensing for Better Two-Way Communication in Remote Learning Environments ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | One of the challenges in remote learning is to allow students to communicate effectively with the lecturer. For example, when a student asks a question, communication will be more effective if the instructor has a zoomed view of the student’s face, so that s/he can interpret expressions etc. The goal of this project is to apply attentive sensing technology (www.elderlab.yorku.ca) to this problem. This technology is able to monitor a large environment such as a classroom and direct a high-resolution ‘attentive’ sensor to events of interest. In particular, working with a senior graduate student or postdoctoral fellow, the successful applicant will: | ||
- | |||
- | Study the problem of detecting hand-raises in the preattentive sensor stream | ||
- | Implement algorithms for detecting hand-raises based upon this investigation | ||
- | Evaluate these algorithms in a real-classroom setting, using proprietary attentive sensing technology | ||
- | |||
- | **Required Background: | ||
- | |||
- | ====== Attentive Sensing for Sport Video Recording Markets ====== | ||
- | |||
- | **Supervisor**: | ||
- | |||
- | The goal of this project is to modify York University’s patented attentive sensor technology to the sport video recording market. Specific application domains under investigation include skiing, indoor BMX parks, and horse tracks. The general problem is to use attentive sensing technology (www.elderlab.yorku.ca) to visually detect and track multiple moving agents (e.g., skiers, riders, horses) and to select specific agents for active high-resolution smooth pursuit. The student will work with senior graduate students, postdoctoral fellows and research scientists to help modify the attentive sensing technology to operate in these domains. Specific tasks include: 1. Ground-truth available datasets 2. Evaluate current attentive algorithms on these datasets 3. Modify these algorithms to improve performance on these datasets. | ||
- | |||
- | **Required Background: | ||
- | |||
- | ====== JPF in a Jar ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | JPF, which is short for Java PathFinder, is an open source tool that has been developed at NASA's Ames Research Center. The aim of JPF is to find bugs in Java code. Instead of using testing to find those bugs, JPF uses model checking. The facts that JPF is downloaded hundreds of times per month and that some of the key papers on JPF have been cited more than a thousand times reflect the popularity of JPF. In fact it is the most popular model checker for Java. | ||
- | |||
- | A study done by Cambridge University in 2014 found that the global cost of debugging code has risen to $312 billion annually. Furthermore, | ||
- | |||
- | Installing JPF is far from trivial. The tool itself has been implemented in Java. Therefore, it should, in theory, be feasible to encapsulate JPF in a Java archive (jar) file. This would make it significantly simplifying the installation process of JPF and, therefore, make the tool more easily accessible to its potential users. | ||
- | |||
- | The aim of this project is to attempt to put JPF in a jar. Since JPF relies on a number of configuration files, so-called Java properties files, incorporating these properly into the jar is one of the challenges. Setting JPF's classpath is another challenge. Since JPF changes almost on a daily basis, our modifications to JPF should ideally be limited to only a few classes, yet another challenge. | ||
- | |||
- | In this project you may collaborate with graduate students of the DisCoVeri group (discoveri.eecs.yorku.ca) and computer scientists of NASA. For more information, | ||
- | |||
- | **Required Background: | ||
- | |||
- | ====== Model-based Design and Development of Embedded Systems with Code Generation Tools ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | Model-based design with code generation tools can be used for simulation, rapid prototyping, | ||
- | |||
- | **Required Background: | ||
- | |||
- | ====== C2000 Concerto Microcontrollers ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | |||
- | The C2000 Concerto family of microcontrollers combines two cores on a single-chip with on-chip low latency interprocessor communication between the two cores: a C28x 32-bit control core for real-time control with faster/more loops and small sampling window; and an ARM 32-bit Cortex-M3 host core for communications and general purpose. The selected student will evaluate the capabilities of the C2000 Concerto family of microcontrollers through testing and investigating open source software for real-time control applications that runs on C2000 Concerto Microcontrollers. | ||
- | |||
- | **Required Background: | ||
- | |||
- | ====== Real-Time Bidding Platform ====== | ||
- | |||
- | |||
- | **Supervisor: | ||
- | |||
- | Description: | ||
- | |||
- | **Required Background: | ||
- | |||
- | |||
- | ====== Circuit and Board Design for a Pulsed Ground Penetrating Radar ====== | ||
- | |||
- | |||
- | **Supervisor: | ||
- | |||
- | The project requires the construction of components for a ground penetrating radar. The students would have to design microwave boards for the high-frequency components of this unit, on both the transmitter and the receiver. On the transmitter side the board would take a 5-MHz input clock, run it through a series of off-the-shelf amplifiers and then through a shaping circuit that would convert the input into an outgoing series of pulses (still at 5-MHz repetition rate) less than 400-ps in duration each. The bandwidth of the signal is roughly 2-8 GHz and hence requires very careful board layout. The receiver would be a time-shifted sampler, used to sample the returning pulses in progressive periods. This radar circuit is ultimately intended to be positioned on a rover doing ground analysis. | ||
- | |||
- | **Required Background: | ||
- | |||
- | |||
- | |||
- | ====== Tilt Target Selection on Touchscreen Phones ====== | ||
- | |||
- | |||
- | **Supervisor: | ||
- | |||
- | Touchscreen mobile devices commonly use a built-in accelerometer to sense movement or tilting actions of the device. Tilt is commonly used the change the orientation of the display between portrait and landscape. Gaming is another common use for tilting actions. However, tilt may also be used for target selection, as a replacement for touch. This research project will evaluate tilt as an input primitive for target selection on touchscreen mobile devices. | ||
- | |||
- | Readings: MacKenzie, I. S., & Teather, R. J. (2012). FittsTilt: The application of Fitts’ law to tilt-based interaction. Proceedings of the Seventh Nordic Conference on Human-Computer Interaction – NordiCHI 2012, pp. 568-577. New York: ACM. | ||
- | |||
- | **Required Background: | ||
- | |||
- | ====== Enabling SaaS access to an experimental AI planner ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | This project involves enriching and integrating a set of fairly complex scripts, which are components of an Artificial Intelligence (AI) planner, and exporting them to the public in a Software-as-a-Service (SaaS) fashion. | ||
- | |||
- | The components are various Unix executables and LISP programs that need to interact in complex ways. The components may be residing in different servers in different universities. Currently integration is performed manually, at the expense of usability. Thus, we aim at constructing a module that: (a) integrates involved components to deliver output in one call, (b) exports a unique web interface (preferably following WSDL/SOAP) to be easily accessed by custom front-end tools by anyone, anywhere, (c ) offers a simple front-end for human users. | ||
- | |||
- | |||
- | **Required Background: | ||
- | |||
- | |||
- | ====== Predicting Angular Error in Rigid Registration ====== | ||
- | |||
- | |||
- | **Supervisor: | ||
- | |||
- | Registration is a fundamental step in image-based surgical navigation. Several (seemingly) different approaches for predicting distance errors in registration are known, but for some surgical procedures, the angular error in registration is more important. This project will validate an approach for predicting angular error in registration; | ||
- | |||
- | ====== Calibration of a Tracked Pointer ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | Description: | ||
- | |||
- | ====== Simulation for Forest Fire Detection ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | Detection of forest fires is a challenging activity that requires considerable training. The objective of this project is to implement a virtual reality simulation to incorporate key aspects of this task and then to perform an evaluation with a small user study. | ||
- | |||
- | |||
- | **Required Background: | ||
- | |||
- | **Recommended Background: | ||
- | |||
- | ====== Study of self-motion perception in microgravity ====== | ||
- | |||
- | |||
- | **Supervisor: | ||
- | |||
- | This is a computer graphics project to present visual motion stimuli to an observer. The software will experimentally control scene content, collect user responses and control the camera trajectory to simulate the desired self-motion profile. | ||
- | |||
- | **Required Background: | ||
- | |||
- | **Recommended Background: | ||
- | |||
- | ====== Stereoscopic cinema calculator ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | Directors of three-dimensional movies sometimes use ' | ||
- | |||
- | **Required Background: | ||
- | |||
- | **Recommended Background: | ||
- | |||
- | ====== Computer pointing devices and the speed-accuracy tradeoff ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | **Required Background: | ||
- | |||
- | **Recommended Background: | ||
- | |||
- | ====== One key text entry ====== | ||
- | |||
- | |||
- | **Supervisor: | ||
- | |||
- | **Required Background: | ||
- | |||
- | Recommended Background: Interest in user interfaces and human-computer interaction (HCI). Understanding of experiment design. Experience in doing user studies. | ||
- | |||
- | ====== The Algorithmics Animation Workshop ====== | ||
- | |||
- | |||
- | **Supervisor: | ||
- | |||
- | The URL for Algorithmics Animation Workshop (AAW) is http:// | ||
- | |||
- | **Required background: | ||
- | |||
- | **Recommended background: | ||
- | |||
- | |||
- | ====== Automated Reasoning System for Quantified Propositional Logic ====== | ||
- | |||
- | |||
- | **Supervisor: | ||
- | |||
- | Quantified Propositional Logics (QPL) plays an important role in a number of computer science disciplines from the theoretical computer science to knowledge representation and verification. There are also a number of open problems concerning this logic, and formulated more than 70 years ago, that can be finally solved (or at least approached) using automated reasoning techniques. The first step in such investigations has to be the design and implementation of a theorem prover, or automated reasoning system, for QPL. Such a system should, in principle, be able to determine whether or not a given formula of QPL is a theorem (or a tautology) in this logic. | ||
- | |||
- | The theorem prover for QPL is to be designed, implemented, | ||
- | |||
- | Background: Various variants of QPL have been formally formulated for the first time in the 1920s by a number of logicians and mathematicians. In modern computer science, QPL plays a significant role in theoretical computer science (proof complexity, satisfiability) as well as in verification and AI. | ||
- | |||
- | **Required background: | ||
- | |||
- | **Recommended background: | ||
- | |||
- | ====== NABU Network Emulator ====== | ||
- | |||
- | **Supervisor: | ||
- | |||
- | Have you ever considered writing your own emulator of an interesting system? There has been a substantial activity in building software emulators of historically significant computers, game consoles, and, recently, smart communication devices. As a result, there is at least one emulator of almost every significant system. This activity contributes, | ||
- | |||
- | Background : The NABU Network was designed and implemented by a Canadian company NABU Manufacturing between 1981 and 1983. The underlying idea behind the network was to link home personal computers to cable television networks which would supply a continuous, high speed stream of computer programs and information (at the rate of 6.5 Mbits per second) to almost an unlimited number of users. Cable television was a uniquely ideal technology for NABU to deliver software and data to home computers because of its high bandwidth and networking capabilities. After the official launch on Ottawa Cablevision in October of 1983, the NABU Network was introduced by Ottawa' | ||
- | |||
- | **Required background: | ||
- | |||
- | **Recommended background: |
projects.1535557066.txt.gz · Last modified: 2018/08/29 15:37 by lesperan