In recent years, bit-precise reasoning has gained importance in

hardware and software verification. Of renewed interest is the use of

symbolic reasoning for synthesising loop invariants, ranking functions,

or whole program fragments and hardware circuits. Solvers for the

quantifier-free fragment of bit-vector logic exist and often rely on

SAT solvers for efficiency. However, many techniques require

quantifiers in bit-vector formulas to avoid an exponential blow-up

during construction. Solvers for quantified formulas usually flatten

the input to obtain a quantified Boolean formula, losing much of the

word-level information in the formula. We present a new approach based

on a set of effective word-level simplifications that are

traditionally employed in automated theorem proving, heuristic

quantifier instantiation methods used in SMT solvers, and model

finding techniques based on skeletons/templates. Experimental results on two

different types of benchmarks indicate that our method outperforms the

traditional flattening approach by multiple orders of magnitude of runtime.

PDF file

In  Formal Methods in System Design

Publisher  Springer

Details