Princeton University

School of Engineering & Applied Science

Scaling Verification by Leveraging Parametrization

Speaker: 
Divjyot Sethi
Location: 
J-401
Date/Time: 
Thursday, September 25, 2014 - 3:00pm to 4:30pm

<strong>Abstract:</strong>
 
Hardware and software systems have become increasingly complex. Many such systems utilize a large number of repeated components which operate in parallel to achieve high performance. Examples include data centers, multi-core processors, and parallel programs. While systems of such scale are highly efficient, their efficiency comes at the cost of increased complexity. These systems tend to be highly error-prone, with the errors being hard to discover.
In this talk I will present my thesis research on proving correctness of such large scale hardware and software systems utilizing multiple repeated components. In particular, I will show how specialized mathematical abstractions can be leveraged to establish correctness of such systems, for any number of such replicated components. In the talk, I will focus on the case study of hardware protocols leveraged in multi-core processors, to present these ideas. Next, I will also briefly describe two other case studies, concurrent software and data center networks, where these ideas were applied for establishing correctness.