<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: arial,helvetica,sans-serif; font-size: 12pt; color: #000000'><div style="color:#000;font-weight:normal;font-style:normal;text-decoration:none;font-family:Helvetica,Arial,sans-serif;font-size:12pt;"><style>p { margin: 0; }</style><div style="font-family: arial,helvetica,sans-serif; font-size: 12pt; color: #000000"><div style="color:#000;font-weight:normal;font-style:normal;text-decoration:none;font-family:Helvetica,Arial,sans-serif;font-size:12pt;"><style>p { margin: 0; }</style><div style="font-family: arial,helvetica,sans-serif; font-size: 12pt; color: #000000"><h1 class="page__title title" id="page-title">Software Verification: Locks and MLoCs*<br></h1><div><span class="event-speaker">
<a href="http://www.nec-labs.com/%7Eagupta/" target="_blank">Aarti Gupta</a> </span>
<span class="event-speaker-from">
(<a href="http://www.nec-labs.com/" target="_blank">NEC Labs America</a>)</span><br><span></span>Wednesday, April 2, 4:30pm<br>Computer Science 105<br><br><p>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.</p><p><br></p><p>*MLoC: Million Lines of Code</p><p><br></p><p>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.</p></div></div></div></div><br></div><br></div></body></html>