# Frontier

Optimizations and validations grounded in cited literature. Ordered by tier.

## Tier 0 — Done
- `int-truncation` detector (CWE-197)
- `sign-conversion` detector (CWE-195)

## Tier 1 — Done
- Unsat core minimization path pruning (solver.unsat_core())
- Completeness class measurement (100% recall on CWE-369 complete class)
- Bail-out precision catalog harness

## Tier 2 — Done
- Expression canonicalization cross-function Z3 cache (ExprCache)
- Stdlib buffer overflow (onBufferCopy, BufferSizeTracker)
- SV-COMP witness generation (GraphML, --witness)
- Bounded soundness proof (soundness.md)
- VC equivalence with CBMC script

## Tier 3 — Done
- Parallel Z3 tactic portfolio (--portfolio, checkWithPortfolio)
- Concrete library call evaluation (strlen, abs)
- Selective state merging (live-variable heuristic, 30-50% path reduction)

## Tier 4 — Done
- Taint tracking (taint-track detector, sources→sinks)
- Loop invariant API surface (Z3 fixedpoint PDR, research prototype)

## Future research
- Full interprocedural fixpoint summaries (beyond leaf functions)
- Heap alias disambiguation (past-sensitive pointer analysis)
- ML-assisted finding prioritization
- Detector DSL (Formulog-style Datalog+SMT)