Details

Autor(en) / Beteiligte

• Fedyukovich, Grigory
• Kaufman, Samuel J.
• Bodik, Rastislav

Titel

Sampling invariants from frequency distributions

Ist Teil von

• 2017 Formal Methods in Computer Aided Design (FMCAD), 2017, p.100-107

Ort / Verlag

FMCAD Inc

Erscheinungsjahr

2017

Quelle

IEEE Xplore

Beschreibungen/Notizen

• We present a new SMT-based, probabilistic, syntax-guided method to discover numerical inductive invariants. The core idea is to initialize frequency distributions from the program's source code, then repeatedly sample lemmas from those distributions, and terminate when the conjunction of learned lemmas becomes a safe invariant. The sampling process gets further optimized by priority distributions fine-tuned after each positive and negative sample. The stochastic nature of this approach admits simple, asynchronous parallelization. We implemented and evaluated this approach in a tool called FreqHorn which shows competitive performance on well-known linear and some non-linear programs.