Unbounded vs. Bounded Verification

Unbounded vs. Bounded Verification

Whenever we want to verify a program, we have to choose a suitable verification approach. Very powerful ones like deductive verification give us strong, unbounded guarantees but are typically hard to apply and require expert knowledge. Highly automated approaches like bounded model checking are very easy to use but only provide bounded guarantees. In practice this means, that unbounded verification of large projects is often not feasible.

During my current research, I study the connection between bounded and unbounded proofs.