Learning inductive invariants by sampling from frequency distributions

被引:4
|
作者
Fedyukovich, Grigory [1 ]
Kaufman, Samuel J. [2 ]
Bodik, Rastislav [2 ]
机构
[1] Florida State Univ, Tallahassee, FL 32306 USA
[2] Univ Washington, Seattle, WA 98195 USA
关键词
Software verification; Invariant synthesis; Syntax-guided synthesis;
D O I
10.1007/s10703-020-00349-x
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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.
引用
收藏
页码:154 / 177
页数:24
相关论文
共 50 条
  • [1] Learning inductive invariants by sampling from frequency distributions
    Grigory Fedyukovich
    Samuel J. Kaufman
    Rastislav Bodík
    Formal Methods in System Design, 2020, 56 : 154 - 177
  • [2] Sampling Invariants from Frequency Distributions
    Fedyukovich, Grigory
    Kaufman, Samuel J.
    Bodik, Rastislav
    PROCEEDINGS OF THE 17TH CONFERENCE ON FORMAL METHODS IN COMPUTER AIDED DESIGN (FMCAD 2017), 2017, : 100 - 107
  • [3] Learning the Boundary of Inductive Invariants
    Feldman, Yotam M. Y.
    Sagiv, Mooly
    Shoham, Sharon
    Wilcox, James R.
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2021, 5 (POPL):
  • [4] The evolution of frequency distributions: Relating regularization to inductive biases through iterated learning
    Reali, Florencia
    Griffiths, Thomas L.
    COGNITION, 2009, 111 (03) : 317 - 328
  • [5] Inferring Inductive Invariants from Phase Structures
    Feldman, Yotam M. Y.
    Wilcox, James R.
    Shoham, Sharon
    Sagiv, Mooly
    COMPUTER AIDED VERIFICATION, CAV 2019, PT II, 2019, 11562 : 405 - 425
  • [6] Formula Slicing: Inductive Invariants from Preconditions
    Karpenkov, Egor George
    Monniaux, David
    HARDWARE AND SOFTWARE: VERIFICATION AND TESTING, HVC 2016, 2016, 10028 : 169 - 185
  • [7] MAPPINGS AND INDUCTIVE INVARIANTS
    JUNG, CFK
    COLLOQUIUM MATHEMATICUM, 1973, 28 (01) : 29 - 31
  • [8] On-Demand Sampling: Learning Optimally from Multiple Distributions
    Haghtalab, Nika
    Jordan, Michael I.
    Zhao, Eric
    ADVANCES IN NEURAL INFORMATION PROCESSING SYSTEMS 35, NEURIPS 2022, 2022,
  • [9] AN INDUCTIVE PROOF OF THE SAMPLING DISTRIBUTIONS FOR THE MLES OF THE PARAMETERS IN AN INVERSE GAUSSIAN DISTRIBUTION
    SCHWARZ, CJ
    SAMANTA, M
    AMERICAN STATISTICIAN, 1991, 45 (03): : 223 - 225
  • [10] The near-irrelevance of sampling frequency distributions
    Bretthorst, GL
    MAXIMUM ENTROPY AND BAYESIAN METHODS, 1999, 105 : 21 - 46