CIS Seminar, Aarti Gupta
Software Verification: Locks and MLoCs*
Aarti Gupta,
NEC Labs America
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. 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 research framework.
*MLoC: Million Lines of Code
Brief Bio:
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 has led research in systems analysis and verification. She has given several invited keynotes highlighting their foundational research contributions in verification and 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.
Thursday, June 19, 2014 at 10:30am
Smith Hall, 102A
Smith Hall, University of Delaware, Newark, DE 19716, USA
- Event Type
- Calendar
- Group
- ENGR - Computer & Information Sciences
- Contact Email
- Contact Name
-
Chien-Chung Shen
- Subscribe
Recent Activity
No recent activity