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.
Yakir Vizel, Princeton University