Learning inductive invariants by sampling from frequency distributions
- PDF / 730,196 Bytes
- 24 Pages / 439.37 x 666.142 pts Page_size
- 49 Downloads / 211 Views
Learning inductive invariants by sampling from frequency distributions Grigory Fedyukovich1
· Samuel J. Kaufman2 · Rastislav Bodík2
Published online: 16 November 2020 © Springer Science+Business Media, LLC, part of Springer Nature 2020
Abstract Automated verification for program safety is reduced to the discovery safe inductive invariants, i.e., formulas that over-approximate the sets of reachable program states, but precise enough to prove unreachability of the error state. We present a framework, called FreqHorn, that follows the Syntax-Guided Synthesis paradigm to iteratively sample candidate invariants from a formal grammar and check them with an SMT solver. FreqHorn automatically constructs grammars based on either source code or bounded proofs. After each (un-)successful candidate, FreqHorn adjusts the grammars to ensure the candidate is not sampled again. The process continues either until the conjunction of successful candidates (called lemmas) is sufficient, or the search space is exhausted. Additionally, FreqHorn keeps a history of counterexamples-to-induction (CTI) which block learning a lemma. With some periodicity, it checks if there is a CTI which is invalidated by the currently learned lemmas and rechecks the failed lemma if needed. FreqHorn is able to check several candidates at the same time to filter them effectively using the well known Houdini algorithm. Keywords Software verification · Invariant synthesis · Syntax-guided synthesis
1 Introduction State-of-the-art techniques for automated program verification certify their outcomes with formal proofs. When verifying a program for safety, such a proof is an inductive invariant [1,3,7,14,25–27,29–31,33,37,40,42–46,48,55] which intuitively describes that no error state is ever reachable. Automated discovery of inductive invariants necessitates exploring a large search space and relies on decision procedures and solvers for Satisfiability Modulo
B
Grigory Fedyukovich [email protected] Samuel J. Kaufman [email protected] Rastislav Bodík [email protected]
1
Florida State University, Tallahassee, USA
2
University of Washington, Seattle, USA
123
Formal Methods in System Design (2020) 56:154–177
155
Theories (SMT). Existing synthesizers are based on Counterexample-Guided Abstraction Refinement (CEGAR) [10], Counterexample-Guided Inductive Synthesis (CEGIS) [53], Property Directed Reachability (PDR) [6,15], Machine Learning [52], but currently, there is no clear witness that any of these approaches consistently outperforms the others. This article gives an overview of the approach to synthesize inductive invariants, called FreqHorn, which is based on Syntax-Guided Synthesis (SyGuS) [2]. FreqHorn is an enumeration-based approach that discovers conjunctive invariants. Each conjunct considered during the verification process belongs to some formal grammar and can be checked individually for the invariance using an SMT solver (we call it a lemma, if it is checked successfully). Our key insight is that a formal grammar need not nece
Data Loading...
