The Taub Faculty of Computer Science Events and Talks

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.