Automated formal verification of programs handling unbounded loops is reduced to finding safe inductive invariants that over-approximate the sets of reachable states, but precise enough to prove unreachability of the error state. Successful solutions to this problem include Counterexample-Guided Abstraction Refinement and Property Directed Reachability, but they are not guaranteed to deliver appropriate invariants. We aim at learning inductive invariants in an "enumerate-and-check" manner, and in particular we exploit the syntactical constructions which appear in the source code to iteratively obtain partial invariants (called lemmas).
The talk will 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. This approach is implemented in a tool called FreqHorn which shows competitive performance on a range of programs.
Presenter: Gregory Fedyukovitch
Wednesday, June 6, room 405, Faculty of Mathematics and Mechanics SPBSU.