Time+Place: Thursday 19/01/2017 10:30 Room 601 Taub Bld.
Title: Achieving Scalable Formal Verification through Generalization and Abstraction
Speaker: Yakir Vizel - CS-Lecture http://www.cs.technion.ac.il/~yvizel/
Affiliation: Princeton University

Abstract:



Modern computerized systems are complex designs that include hardware 
and software components. Designing and implementing such systems 
requires extensive engineering. Yet, unlike other domains of 
engineering, software and hardware engineers often lack the mathematical 
tools to help them specify the requirements and verify that the 
implementation conforms to the specification. Formal Methods aim at 
bridging this gap. In particular, Formal Verification (FV) techniques 
supply the tools needed to either prove the correctness, reliability and 
security of computerized systems, or find erroneous behaviors. However, 
the application of FV techniques to real-life designs is often 
challenging.

One widely used automated FV technique is Model Checking (MC). While MC 
has been successfully applied by leading companies as part of their 
design methodology, it still suffers from scalability constraints that 
limit its usage.

In this talk, we will present our latest contributions and efforts in 
overcoming scalability constraints. These efforts require improvements 
of MC algorithms, as well as to the overall FV methodology in which MC 
is applied. We will present our SAT-based MC algorithm, AVY, explaining 
the concepts and ideas that make it a top-tier MC algorithm. We will 
then introduce our Instruction-Level Abstraction (ILA) methodology for 
system-on-chip verification, and its applications in verification of 
security properties. We will conclude with our future endeavors for 
increasing the capacity of MC and further improving the applicability of 
FV.


Short Bio:

Yakir Vizel is Postdoctoral Research Associate at Princeton University 
working under the supervision of Prof. Sharad Malik at the Electrical 
Engineering Department. He has received a B.Sc. in Mathematics and CS 
from the Technion and a Ph.D. in CS from the Technion - working with 
Prof. Orna Grumberg on SAT-based Model Checking. He has worked on 
developing Formal Verification algorithms of hardware verification at 
Intel, Jasper Design Automation, Cadence, and, currently, at Mellanox.