Skip to main content

cegar_verify

logicaffeine_verify::abstraction

Function cegar_verify 

Source 
pub fn cegar_verify(
    init: &VerifyExpr,
    transition: &VerifyExpr,
    property: &VerifyExpr,
    initial_predicates: &[VerifyExpr],
    max_refinements: u32,
) -> AbstractionResult
Expand description

CEGAR verification loop: abstract, check, refine.

  1. Build abstract model from current predicates
  2. Check abstract model with k-induction
  3. If abstract model is safe, return Safe
  4. If abstract counterexample found, check concreteness via BMC
  5. If concrete, return Unsafe
  6. If spurious, extract new predicates from the counterexample and refine