Software Verification: Locks and MLoCs*

Software verification deals with proving or falsifying correctness properties of programs, and has broad applications from ensuring safety of mission-critical software to improving program robustness and programmer productivity. This area has long held theoretical interest, but the inherent undecidability of the general problem and intractability of specific formulations have been barriers to practical success. Approaches based on automatic techniques for state space exploration, such as model checking and symbolic execution, have seen a resurgence of interest in recent years, driven largely by advancements in solvers for Boolean Satisfiability (SAT) and Satisfiability Modulo Theories (SMT). These solvers perform the underlying search for proofs or bugs, typically by reasoning over abstract models of programs. While abstraction is critical in scaling to real-life programs, it is equally important to ensure enough precision in the models and the analysis to verify specific properties of interest. In this talk, I will describe my work in foundational techniques that address these twin challenges of precision and scalability in verifying sequential and multi-threaded programs. I will also share the lessons learnt in my efforts in driving them to industry practice where they are routinely used in a modular methodology to find complex bugs in software projects, some with millions of lines of code. Finally, I will discuss future extensions and applications of this verification framework.

*MLoC: Million Lines of Code

Aarti Gupta received her PhD in Computer Science from Carnegie Mellon University. Her broad research interests are in the areas of formal analysis of programs/systems and automatic decision procedures. At NEC Labs she leads research in systems analysis and verification. She has given several invited keynotes highlighting the foundational research contributions of her group in verification and their successful industrial deployment. She has served as an Associate Editor for Formal Methods in System Design (since 2005) and for the ACM Transactions on Design Automation of Electronic Systems (2008-2012). She has also served as Co-Chair for the International Workshop on Satisfiability Modulo Theories (SMT) 2010, the International Conference on Computed Aided Verification (CAV) 2008, and Formal Methods in Computer Aided Design (FMCAD) 2006. She is currently serving on the Steering Committee of CAV.