Research Areas

In an increasingly technologically-driven world, there is infinite demand for computer speed and security. ECE researchers are improving many aspects of software and hardware to meet these demands. We are improving system reliability by automatically verifying designs, exploiting the efficiencies of multiple cores, and using software to protect the hardware itself from hackers.

Current Research

Equivalence Checking

Nearly all designs require many iterations of optimization, and it is important to check that the design remains the same at each stage. Checking for equivalence in sequential designs is difficult, due to the size of the state space and the fact that the optimized design might have a drastically different set of state variables and encoding. We are working to solve this problem by finding non-trivial static and inductive invariants.

Fault Diagnosis

Semiconductor companies rely on effective tests to distinguish good parts from defective ones, and some defective parts are easier to diagnose than others. Our work explores various strategies to quickly diagnose and root-cause the errors without using traditionally expensive techniques.

Design Verification & Swarm Intelligence

Verification and validation is a critical bottleneck in the design of complex hardware systems, and insufficient verification can compromise both the reliability and security of the system. Virginia Tech research combines swarm-aggregate learning with parallel search to significantly reduce the computational costs.

Multicore Improvements

ECE researchers are working on a variety of projects (including Popcorn Linux) that will improve computer speeds and efficiency by optimizing the use of multicore technologies.

We are developing techniques to automatically transform legacy sequential programs to make use of multicore technology. HydraVM is a virtual machine implementation that refactors sequential programs through program analysis techniques and speculative transactional execution, and transforms sequential code into high-performance parallel code.

We are also developing real-time resource management techniques and implementations for virtualized environments, targeting multicore architectures. KairosVM is a KVM-based virtualization infrastructure that enables real-time applications and their underlying operating systems to be virtualized on multicore architectures without any modifications, while satisfying application time constraints.

With concurrent data structures becoming increasingly widespread, linearizability (the de facto correctness criterion) and its various quantitative relaxations allow more freedom in implementation for performance optimization. We are developing fully automated static and runtime verification techniques for checking standard and relaxed linearizability conditions.

S.C. Sniffer

Embedded computing devices often leak information about the software code that they execute, either through power and heat dissipation or electromagnetic radiation. Such side-channel information can be exploited by an adversary to deduce information such as passwords and cryptographic keys. We are developing new program analysis and synthesis techniques to transform today's manually secured and verified systems into automatically secured and verified systems.