projects
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revision | ||
projects [2017/08/10 19:17] – jenkin | projects [2018/05/07 14:39] (current) – peterlian | ||
---|---|---|---|
Line 1: | Line 1: | ||
~~NOTOC~~ | ~~NOTOC~~ | ||
====== Proposed Projects | ====== Proposed Projects | ||
+ | |||
+ | ====== Detecting and visulizing anomalies in dynamic networks ====== | ||
+ | **Supervisor: | ||
+ | |||
+ | In this project, the goal is to detect and visualize anomalies in dynamic graphs. Graphs are powerful tools to model networks and relationships between their entities. Many of the real-world graphs are dynamic in which nodes and edges are being added and deleted over time. Some of the dynamic network examples include social networks and computer networks. Anomalies are any deviation from the normal. For example, in a computer network, communications are normal over time until a single machine is attacked by a large number of other machines at a specific time point. We work on finding time points that an anomaly occurs and nodes, edges or subgraphs that are responsible for this anomalous behavior. This project focuses on finding and visualizing anomalies in a stream of graphs. The student will first use a visualization tool to visualize the network over time. This helps in better understanding the changes in the structure of the network. There are various visualization tools available to use for this purpose. In the second phase, the student will implement a graph anomaly detection method and combine it with the visualzation program so that the graph stream can be monitored through visualization and anomalies can be detected and illustrated in an online fashion. This project is a part of a collaborative project with IBM and the student will work closedly with a PhD student in the project. | ||
+ | |||
+ | **Required skills:** Good programming skills in Python and Java. | ||
+ | |||
+ | **Recommended skills:** Experience with visualization tools is very helpful, Interest in algorithms for graphs. | ||
+ | |||
+ | ====== Graphical User Interface for Power System Simulator ====== | ||
+ | **Supervisor: | ||
+ | |||
+ | 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/ | ====== Ultrasound simulation/ | ||
Line 186: | Line 241: | ||
**Supervisor: | **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, | 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, | ||
Line 194: | Line 247: | ||
- | Attentive Sensing for Better Two-Way Communication in Remote Learning Environments | + | ====== |
- | Supervisor: James Elder | + | **Supervisor:** James Elder |
- | + | ||
- | Required Background: General CSE408x prerequisites, | + | |
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: | 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: | ||
Line 205: | Line 256: | ||
Implement algorithms for detecting hand-raises based upon this investigation | Implement algorithms for detecting hand-raises based upon this investigation | ||
Evaluate these algorithms in a real-classroom setting, using proprietary attentive sensing technology | Evaluate these algorithms in a real-classroom setting, using proprietary attentive sensing technology | ||
- | Attentive Sensing for Sport Video Recording Markets | ||
- | Supervisor: James Elder | + | **Required Background:** General CSE408x prerequisites, |
- | Required Background: Good programming skills; Good math skills; Knowledge of C and MATLAB programming languages | + | ====== Attentive Sensing for Sport Video Recording Markets ====== |
- | 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 | + | **Supervisor**: James Elder |
+ | 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. | ||
- | JPF in a Jar | + | **Required Background: |
- | Supervisor: Franck van Breugel | + | ====== JPF in a Jar ====== |
- | Description: 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. | + | **Supervisor:** Franck van Breugel |
+ | |||
+ | 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, | A study done by Cambridge University in 2014 found that the global cost of debugging code has risen to $312 billion annually. Furthermore, | ||
Line 228: | Line 281: | ||
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, | 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: General CSE408x prerequisites | + | **Required Background:** General CSE408x prerequisites |
- | Model-based Design and Development of Embedded Systems with Code Generation Tools | + | ====== |
- | Supervisor: Jia Xu | + | **Supervisor:** Jia Xu |
- | + | ||
- | Required Background: At least a B+ in Embedded Systems (CSE3215), MATLAB, C programming skills, solid experience in using a microcontroller such as Arduino. | + | |
- | + | ||
- | Project Description: | + | |
Model-based design with code generation tools can be used for simulation, rapid prototyping, | Model-based design with code generation tools can be used for simulation, rapid prototyping, | ||
+ | **Required Background: | ||
+ | ====== C2000 Concerto Microcontrollers ====== | ||
- | C2000 Concerto Microcontrollers | + | **Supervisor: |
- | Supervisor: Jia Xu | ||
- | Required Background: At least a B+ in Embedded Systems (CSE3215), strong C programming skills, solid knowledge | + | 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 |
- | Description: 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 | + | **Required Background:** At least a B+ in Embedded Systems (EECS3215), strong C programming skills, solid knowledge |
+ | ====== Real-Time Bidding Platform ====== | ||
- | Real-Time Bidding Platform | + | **Supervisor:** Jia Xu |
- | + | ||
- | Supervisor: Jia Xu | + | |
- | + | ||
- | Required Background: At least a B+ in Operating System Fundamentals (CSE3221), strong Ubuntu/ | + | |
Description: | Description: | ||
+ | **Required Background: | ||
- | Circuit and Board Design for a Pulsed Ground Penetrating Radar | + | ====== |
- | Supervisor: | ||
- | Description: 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. | + | **Supervisor:** Sebastian Magierowski |
- | Required Background A background in undergraduate-level electronics is very important. Experience with board level implementations | + | 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 |
+ | **Required Background: | ||
+ | ====== Tilt Target Selection on Touchscreen Phones ====== | ||
- | Proposed Projects from Previous Years | + | **Supervisor:** Scott MacKenzie |
- | + | ||
- | Tilt Target Selection on Touchscreen Phones | + | |
- | + | ||
- | Supervisor: Scott MacKenzie | + | |
- | + | ||
- | Required Background: General 4080 prerequisites, | + | |
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. | 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. | ||
Line 288: | Line 330: | ||
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. | 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. | ||
- | Attentive Sensing for Better Two-Way Communication | + | **Required Background: |
- | Supervisor: James Elder | + | ====== Attentive Sensing for Better Two-Way Communication in Remote Learning Environments ====== |
- | Required Background: General CSE408x prerequisites, | + | **Supervisor:** James Elder |
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: | 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: | ||
Line 298: | Line 340: | ||
Study the problem of detecting hand-raises in the preattentive sensor stream | Study the problem of detecting hand-raises in the preattentive sensor stream | ||
Implement algorithms for detecting hand-raises based upon this investigation | Implement algorithms for detecting hand-raises based upon this investigation | ||
- | Evaluate these algorithms in a real-classroom setting, using proprietary attentive sensing technology | + | Evaluate these algorithms in a real-classroom setting, using proprietary attentive sensing technology. |
- | Attentive Sensing for Sport Video Recording Markets | + | |
- | Supervisor: James Elder | + | **Required Background:** General CSE408x prerequisites, |
- | Required Background: Good programming skills; Good math skills; Knowledge of C and MATLAB programming languages | + | ====== Attentive Sensing for Sport Video Recording Markets ====== |
- | 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 | ||
- | Continuation of a Path Diagram to Syntax Application | + | **Supervisor**: |
- | Supervisor: Jeff Edmonds | + | 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: | + | **Required Background:** Good programming skills; Good math skills; Knowledge of C and MATLAB programming languages. |
- | Recommended Background: Java software development | ||
- | Structural equation modeling (SEM) is a statistical technique that is becoming increasingly popular in the educational and behavioral sciences. SEM allows researchers to test the validity of hypothesized models involving complex relationships among multiple variables. Collected data is used to estimate the parameters of the equations and assessing the fit of the model. | ||
- | The software required is an application that allows researchers | + | ====== Enabling SaaS access |
- | To date a promising functional application has been developed in JAVA by a Computer Science student as a 4080 project. The existing software allows the user to draw a path diagram and outputs code for the R package sem. There are a number of improvements to be made (refinements and additions to graphical user interface) and then the application needs to be extended to output syntax appropriate for additional software applications (openMX, MPlus and EQS). Though this project may not begin at “the first stages” of the software lifecycle, this scenario is likely common in the software development market. In addition, the student will be working with a primary “client” who is far less technically advanced, which is also reflective of real-world situations. | + | **Supervisor: |
- | More details here. | + | 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. |
- | Enabling SaaS access | + | 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. |
- | Supervisor: Sotirios Liaskos (liaskos at yorku dot ca) | ||
- | Required Background: Good knowledge of Unix tools / Python, Perl or Awk. Comfort with algorithms and programming. Essential: 2031 – Software Tools. Desired: 3402 – Functional & Logic Programming, | + | **Required Background:** Good knowledge of Unix tools / Python, Perl or Awk. Comfort with algorithms and programming. Essential: 2031 – Software Tools. Desired: 3402 – Functional & Logic Programming, |
- | Description: | ||
- | The components are various Unix executables and LISP programs that need to interact | + | ====== Predicting Angular Error in Rigid Registration ====== |
- | Learning objectives: | ||
- | Understand the technologies and process involved in turning native code into a web-service (“servicizing”). | + | **Supervisor: |
- | Study a state-of-the-art AI planner and understand its workings. | + | |
- | Exercise scripting skills. | + | |
- | Predicting Angular Error in Rigid Registration | + | |
- | Supervisor: Burton Ma | + | 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; |
- | Description: | + | ====== Calibration of a Tracked Pointer ====== |
- | Calibration of a Tracked Pointer | + | **Supervisor:** Burton Ma |
- | + | ||
- | Supervisor: Burton Ma | + | |
Description: | Description: | ||
- | A privacy safeguard framework for sharing photos on Facebook | ||
- | Supervisor: Uyen Trang Nguyen | ||
- | Description: | + | ====== Simulation for Forest Fire Detection ====== |
- | Required prerequisite background: Proficiency in programming, | + | **Supervisor:** Rob Allison |
- | Desired prerequisite: | + | Detection |
- | Simulation for Forest Fire Detection | ||
- | Supervisor: Rob Allison | + | **Required Background:** General |
- | + | ||
- | Required Background: General | + | |
- | + | ||
- | Recommended Background: CSE3431 or CSE4471 or equivalent | + | |
- | + | ||
- | Description | + | |
- | + | ||
- | 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. | + | |
- | + | ||
- | Study of self-motion perception in microgravity | + | |
- | Supervisor: Rob Allison | + | **Recommended Background:** EECS3431 or EECS4471 or equivalent |
- | Required Background: General CSE408x prerequisites | + | ====== Study of self-motion perception in microgravity ====== |
- | Recommended Background: CSE3431 or CSE4471 or equivalent | ||
- | Description | + | **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. | 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. | ||
- | Stereoscopic cinema calculator | + | **Required Background:** General EECS408x prerequisites |
- | + | ||
- | Supervisor: Rob Allison | + | |
- | Required | + | **Recommended |
- | Recommended Background: CSE3431 or CSE4471 or equivalent | + | ====== Stereoscopic cinema calculator ====== |
- | Description | + | **Supervisor: |
Directors of three-dimensional movies sometimes use ' | Directors of three-dimensional movies sometimes use ' | ||
- | Computer pointing devices and the speed-accuracy tradeoff | + | **Required Background: |
- | Supervisor: Scott MacKenzie | + | **Recommended Background:** EECS3431 or EECS4471 or equivalent |
- | Required Background: General 4080 prerequisites, | + | ====== Computer pointing devices |
- | Recommended Background: Interest in user interfaces and human-computer interaction (HCI). Understanding of experiment design. Experience in doing user studies. | + | **Supervisor:** Scott MacKenzie |
- | One key text entry | + | **Required Background: |
- | Supervisor: Scott MacKenzie | + | **Recommended Background:** Interest in user interfaces and human-computer interaction (HCI). Understanding of experiment design. Experience in doing user studies. |
- | Required Background: General 4080 prerequisites, | + | ====== One key text entry ====== |
- | 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: |
- | Supervisor: Andy Mirzaian | + | **Required Background:** General 4080 prerequisites, |
- | Required background: General prerequisites | + | Recommended Background: Interest in user interfaces and human-computer interaction (HCI). Understanding of experiment design. Experience in doing user studies. |
- | Recommended background: CSE 3101 | + | ====== The Algorithmics Animation Workshop ====== |
- | Description | + | |
+ | **Supervisor: | ||
The URL for Algorithmics Animation Workshop (AAW) is http:// | The URL for Algorithmics Animation Workshop (AAW) is http:// | ||
- | Automated Reasoning System for Quantified Propositional Logic | + | **Required background: |
- | Supervisor: Zbigniew Stachniak | + | **Recommended background:** EECS 3101 |
- | Required background: General prerequisites | ||
- | Recommended background: Passion | + | ====== Automated Reasoning System |
- | Description | + | |
+ | **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. | 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. | ||
Line 440: | Line 454: | ||
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. | 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. | ||
- | NABU Network Emulator | + | **Required background: |
- | Supervisor: Zbigniew Stachniak | + | **Recommended background:** Passion for programming and experimentation; |
- | Required background: General prerequisites | + | ====== NABU Network Emulator ====== |
- | Recommended background: Java (including 2D graphics); Some knowledge of PC hardware architecture; | + | **Supervisor:** Zbigniew Stachniak |
- | + | ||
- | Description | + | |
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, | 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' | 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.1502392669.txt.gz · Last modified: 2017/08/10 19:17 by jenkin