Efficient Verification of Multi-Property Designs (The Benefit of Wrong Assumptions) (Extended Version)

Eugene Goldberg, Matthias Gudemann, Daniel Kroening +1

We consider the problem of efficiently checking a set of safety properties P1,....,Pk of one design. We introduce a new approach called JA-verification where JA stands for "Just-As…