Concolic Explorer

[Stevengre]

ConcolicExplorer builds the proof the Checker validates: a concrete seed names one path, the Checker folds it into edges plus a remainder, and that remainder's model is the next seed — repeated until no satisfiable remainder is left.

worklist ← [ (root, get_model(φ)) ]            # an open node + a concrete seed for it
while worklist:
    (node, seed) ← worklist.pop()
    τ ← generate_proof_trace(seed)              # run the seed on the LLVM backend → rule sequence
    S ← node
    loop:
        r ← guided_execute(S, τ)                # fold edges; stop at first SAT remainder or trace end
        record r.edge
        case r:
          SAT remainder (guard g):              # taken rule covers only part of S
            record branch g (→ r.S')
            worklist.push( (node ∧ ¬g, r.model) )   # still-uncovered region: more guards to find
            S, τ ← r.S', τ[r.consumed:]             # continue along the taken branch
          UNKNOWN:
            emit UndecidedObligation; break
          TRACE END:
            close S' (cover to target / loop, terminal, or Failed counterexample); break
# worklist empty ⇒ every remainder unsatisfiable or covered ⇒ all paths covered

Limitations

• Non-deterministic semantics. Concrete execution takes one rule per state (by priority), so it can never witness several rules applying to the same concrete state — hence the deterministic-semantics scope.
• Rules missing from the concrete trace. Some rules never fire in concrete execution (e.g. symbolic-only [symbolic] rules and lemmas), so the LLVM trace cannot name them; the symbolic side must supply them itself. This may need composable symbolic execution to ensure the concolic execution only works for the src without the assume instructions in the test.