System Analysis and Verification (SAVe) Lab

These days hardware and software systems are increasingly being used in safety-critical domains, such as electronic military and medicine equipment and automated transportation systems. This fact makes the accuracy of their analysis very important as an uncaught system bug may endanger human life or lead to a significant financial loss. Traditionally, the verification of these systems has predominantly been accomplished by computer simulation. However, it does not ascertain 100% correctness and thus has primarily been responsible for many unfortunate incidents that happened due to an erroneous hardware or software system deployed in a safety-critical domain. The primary focus of our research is on using formal methods, which are based on mathematical techniques and thus unlike simulation ensure complete results, for the analysis and verification of hardware, software, and embedded systems. In particular, we aim at using theorem proving and model checking, which are the some widely used formal methods, to develop methodologies, algorithms and tools for the accurate analysis of systems that are continuous or random in nature or interact with continuous or random physical environments. Besides the formal verification, we are also involved in designing algorithms and techniques for hardware systems. Some of these ongoing activities cover the domains hardware security, approximate computing, thermal and resource management in many-core systems, surgical robotics and cell biology.