How Hard is Bit-Precise Reasoning?
Gergely Kovásznai · 2018
Formal verification of hardware and software is important in the case of critical systems, as shown by several accidents due to such problems as overflow, rounding error, etc. Bit-precise reasoning over bit-vectors is a fundamental tool for attacking such verification problems.But how hard is reasoning over bit-vector logics?It is essential to answer this question before inventing solving approaches for bit-vector logics.The talk gives an overview on the complexity of bit-vector logics.Complexity depends on what bit-vector operators are used and whether quantifiers are permitted.For instance, the quantifier-free bit-vector logic (QF_BV) with all the common operators is NEXPTIME-complete, which seems extremely high considering the fact that QF_BV is commonly used in hardware verification.We will investigate how that complexity can be reduced to NPcompleteness or PSPACE-completeness by restricting the set of operators.Quantifiers are often used in software verification problems such as termination analysis and invariant synthesis.The bit-vector logic with quantifiers and uninterpreted functions (UFBV) is 2-NEXPTIME-complete.Interestingly, as it was proved recently, that logic without uninterpreted functions (BV) is AEXP(poly)-complete.