Systems Analysis & Verification

Introduction

Our research focuses on analysis and verification of hardware, software, and embedded systems. We envisage that formal methods will become an essential part of the best practices in the design and development of large, open, distributed, general purpose or embedded systems. With the growth of multi-core processing and concurrent programming in many key computing segments (mobile, server, gaming), there is a great need for effective development and verification technologies for concurrent multi-threaded programs. At the same time, due to the ubiquitous availability of cyber systems that interact with physical environments, there is a great need to develop technologies that target the whole system.

The cornerstone of our research is investigation into leading-edge technologies for formal analysis, bringing together the domains of system modeling, formal verification, program analysis, automata theory, constraint solvers, and software engineering. We have made significant progress in these domains in the recent past, with notable examples in SAT-based model checking and software program verification. Going forward, we believe it is essential to combine formal verification with other static and dynamic analysis techniques, with the overall goals of improving design quality, improving developer productivity, and reducing the cost of system development.

Currently, we have the following projects:

• ConSave: Analysis and verification for concurrent systems and programs
• F-Soft: Software verification platform for sequential programs

Older projects:

• Tessa: Techniques for Embedded System and Software Assurance
• VeriSol: Symbolic model checking platform, including SAT-based and SMT-based techniques