Login
Talks & Seminars
Boolean Methods in Computer Reliability and Security
Dr. Sanjit Seshia, UC Berkeley
Date & Time: August 11, 2005 15:00
Venue: EE Seminar Hall
Abstract:
Detecting and correcting errors before run-time is increasingly important in today's ubiquitous computing environment. The effectiveness of logic-based methods for hardware verification and program analysis depends on the efficiency of the underlying decision procedures. As existing procedures do not scale up, verifiers sacrifice modeling precision for scalability. Imprecise modeling results in numerous false alarms and the inability to verify properties that depend on data or timing, in addition to control. I will present an approach that addresses this problem by modeling with first-order logics involving arithmetic and reasoning using new, efficient decision procedures for those logics. In our approach, decision problems involving arithmetic are transformed to problems in the Boolean domain, such as Boolean satisfiability solving, thereby leveraging recent advances in that area. The transformation automatically detects and exploits problem structure. I will briefly describe some of the underlying theory and present experimental results showing that our decision procedures can outperform others by over a factor of 100. The decision procedures form the computational engines for two verification systems, UCLID and TMV. These systems have been applied to problems in computer security, electronic design automation, and software engineering that require efficient and precise analysis of data- and timing-dependent properties. This talk will present two example applications: a semantics-aware detector of viruses and worms that shows greater resilience to obfuscation than commercial tools, and a verifier for self-timed circuits that found an error in a published circuit of a widely-used industrial microprocessor.
Speaker Profile:
Sanjit A. Seshia is an assistant professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received a Ph.D. and an M.S. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in reliable and secure computing, with a current focus on applying automated formal methods to problems in computer security, electronic design automation, and software engineering.
List of Talks

Webmail

Username:
Password:
Faculty CSE IT
Forgot Password
    [+] Sitemap     Feedback