Abstract: The inherent complexity of large-scale software systems has always posed a significant challenge to software researchers and practitioners. On top of this, the ever-growing penetration of software into nearly every aspect of modern life, from mobile banking to healthcare systems, makes its security and dependability more critical than ever. Software verification is known to provide the highest degree of software assurance. Most notably, lightweight formal methods have recently received a lot of attention in the software engineering and security communities due to their automated, yet formally precise, analysis capabilities, which reduce the burden on traditional formal verification techniques. In this talk, I will present the ongoing research in my research group, which explores the possibility of leveraging lightweight formal methods for automated and pragmatic security and dependability analysis of widely-used software systems. I will illustrate the ideas in the context of practical applications, discuss their potential for moving the field forward, and pose essential areas of research in the coming era.

Short Bio: Hamid Bagheri is an Associate Professor in the School of Computing at the University of Nebraska-Lincoln. He is a faculty associate at the Institute for Software Research (ISR), and a co-director of the ESQuaReD Lab. Prof. Bagheri is a recipient of the EPSCoR FIRST Award and the NSF CISE Career Research Initiation Initiative Award. Prior to joining UNL, he was a postdoctoral researcher at the Massachusetts Institute of Technology and the University of California, Irvine. He obtained his Ph.D. in computer science from the University of Virginia. His research interests are in the field of software engineering. To date, his focus has spanned the areas of security analysis, software testing, applied formal methods, software architecture, and dependability analysis. His publications at several conferences have been recognized as best papers. He is currently on the review boards of IEEE Transactions on Software Engineering and ACM Transactions on Software Engineering and Methodology.