HomeSCS Home
School of Computer Science School of Computer Science  
News
EducationResearch People About
 
 
CSD
RI
ISRI
HCII
LTI
CALD
CALD
 
 
 
 

 


SCS DISTINGUISHED LECTURE SERIES
4:00 PM - Wean Hall 7500
3:45 PM Distinguished Donuts - Outside the Hall

SCS Distinguished Dissertation Award Presentation and Lecture

Sanjit A. Seshia
Assistant Professor
Department of Electrical Engineering and Computer Sciences
University of California, Berkeley

Adaptive Eager Boolean Encoding for
Arithmetic Reasoning in Verification

Decision procedures for first-order logics are widely applicable in design verification and static program analysis. However, existing procedures rarely scale to large systems, especially for verifying properties that depend on data or timing, in addition to control.

In this talk, I will describe a new approach for building efficient, automated decision procedures for first-order logics involving arithmetic. The central idea is to transform decision problems involving arithmetic 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 based on new theoretical results and machine learning. The results of experimental evaluations show that our decision procedures can outperform other state-of-the-art procedures by several orders of magnitude.

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 system functionality and timing. The talk will briefly mention some of these applications.

Speaker Bio:

Sanjit A. Seshia is an assistant professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and a Ph.D. 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 dependable computing and computational logic, with a current focus on applying automated formal methods to problems in computer security, electronic design automation, and program analysis.

<< Back

Email

 
HomeSCS Home   ARCHIVES
Contact Info