Dr. Sankaranarayanan is primarily interested in formal verification techniques, especially for hybrid cyber-physical systems (CPS) which model discrete programs interacting with a continuous environment. In this regard, his work explores the application of techniques from areas such as convex optimization, algebraic geometric methods, combinatorial optimization, symbolic and numerical decision procedures to analyze the behavior of programs and verify key temporal properties such as safety, termination, liveness and stability. His recent work applies Monte-Carlo sampling, rare-event simulations and extreme value theory to develop novel verification techniques for cyber-physical systems is ongoing. Finally, his group is actively extending the scope of verification from verifying the software systems to verifying systems with human operators in the loop using cognitive science techniques to understand and model the behavior of human operators.
Symbolic Deadlock Analysis in Concurrent Libraries and their Clients.
Proceedings / IEEE International Conference, Automated Software Engineering ; sponsored by IEEE Computer Society, NASA Ames Research Center, in cooperation with AAAI, ACM SIGART and SIGSOFT. IEEE International Automated Software Enginee....
480-491.
2009
