SHF: Small: Incremental Inductive Verification: A New Direction for Model Checking

University Of Colorado At Boulder, Boulder CO

Investigators

Abstract

Hardware and software computer systems are integrated into many aspects of our society, including medicine, transportation, financial markets, and communication. Thus, the correctness of a computer system can be critical for financial or even human safety reasons. Formal verification is a methodology for finding errors and certifying that a system is free of errors. It complements testing, which in practice can neither cover every possibility nor declare the absence of errors. Because of the increasing complexity and prevalence of computer systems in recent years, significant improvements in algorithms for formal verification now have an immediate impact in computer system development, which in turn decreases design costs, accelerates development, and results in safer equipment. This project builds on the success of the IC3 algorithm for verifying invariance properties of digital hardware. IC3, introduced only two years ago, is already used widely by hardware manufacturers and electronic design automation companies. It is reported that it can, in practice, find deep bugs that are difficult to find with testing, or obtain proofs that no other algorithm can find. But achieving the next significant gain in performance requires moving beyond the bit-level analysis that IC3 performs and instead considering designs at the word level, that is, at a level in which whole registers are sometimes considered rather just than their component latches. This project addresses this challenge by developing a multi-domain version of IC3, as well as abstract domains, for reasoning about equality, uninterpreted functions, and arithmetic properties of circuits. A second component of this project is to extend the incremental, inductive verification (IIV) methodology, of which IC3 was the first instance, to analyze properties expressed in CTL and CTL*, which are logics for expressing branching-time behavior. Increased expressiveness allows analyzing more aspects of a design. A final component is to exploit the natural parallelism of IIV algorithms through a distributed implementation.