scholarly journals Formula Slicing: Inductive Invariants from Preconditions

2016 ◽  
pp. 169-185 ◽  
Author(s):  
Egor George Karpenkov ◽  
David Monniaux
Keyword(s):  
Inductive Invariants

Synthesizing Conjunctive & Disjunctive Linear Invariants by K-means++ and SVM

2020 ◽  
Vol 17 (6) ◽  
pp. 847-856
Author(s):  
Shengbing Ren ◽  
Xiang Zhang
Keyword(s):  
Software Verification ◽  
State Of The Art ◽  
Positive Sample ◽  
Machine Learning Algorithms ◽  
Support Vector ◽  
Hoare Logic ◽  
Excellent Performance ◽  
Automated Software ◽  
Inductive Invariants ◽  
Linear Invariants

The problem of synthesizing adequate inductive invariants lies at the heart of automated software verification. The state-of-the-art machine learning algorithms for synthesizing invariants have gradually shown its excellent performance. However, synthesizing disjunctive invariants is a difficult task. In this paper, we propose a method k++ Support Vector Machine (SVM) integrating k-means++ and SVM to synthesize conjunctive and disjunctive invariants. At first, given a program, we start with executing the program to collect program states. Next, k++SVM adopts k-means++ to cluster the positive samples and then applies SVM to distinguish each positive sample cluster from all negative samples to synthesize the candidate invariants. Finally, a set of theories founded on Hoare logic are adopted to check whether the candidate invariants are true invariants. If the candidate invariants fail the check, we should sample more states and repeat our algorithm. The experimental results show that k++SVM is compatible with the algorithms for Intersection Of Half-space (IOH) and more efficient than the tool of Interproc. Furthermore, it is shown that our method can synthesize conjunctive and disjunctive invariants automatically

Decidability of inferring inductive invariants

2016 ◽  
Author(s):  
Oded Padon ◽  
Neil Immerman ◽  
Sharon Shoham ◽  
Aleksandr Karbyshev ◽  
Mooly Sagiv
Keyword(s):  
Inductive Invariants

scholarly journals Bounded Quantifier Instantiation for Checking Inductive Invariants

2017 ◽  
pp. 76-95 ◽  
Author(s):  
Yotam M. Y. Feldman ◽  
Oded Padon ◽  
Neil Immerman ◽  
Mooly Sagiv ◽  
Sharon Shoham
Keyword(s):  
Quantifier Instantiation ◽  
Inductive Invariants

scholarly journals Strengthening Model Checking Techniques With Inductive Invariants

2009 ◽  
Vol 28 (1) ◽  
pp. 154-158 ◽  
Author(s):  
Gianpiero Cabodi ◽  
Sergio Nocco ◽  
Stefano Quer
Keyword(s):  
Model Checking ◽  
Inductive Invariants

scholarly journals Inductive invariants of closed extensions of mappings

1972 ◽  
Vol 25 (1) ◽  
pp. 73-78 ◽  
Author(s):  
Togo Nishiura
Keyword(s):  
Inductive Invariants

scholarly journals A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines

2020 ◽  
Vol 64 (7) ◽  
pp. 1523-1552
Author(s):  
Daniel Neider ◽  
P. Madhusudan ◽  
Shambwaditya Saha ◽  
Pranav Garg ◽  
Daejun Park
Keyword(s):  
Learning Algorithms ◽  
Separation Logic ◽  
Extended Version ◽  
Conference Paper ◽  
Effective Learning ◽  
Inductive Synthesis ◽  
Fixed Set ◽  
Decidable Theories ◽  
Guided Inductive ◽  
Inductive Invariants

Abstract We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counterexample guided inductive synthesis principle and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates. Moreover, we evaluate our framework in two verification settings, one in which verification engines need to handle quantified formulas and one in which verification engines have to reason about heap properties expressed in an expressive but undecidable separation logic. Our experiments show that our invariant synthesis framework based on non-provability information can both effectively synthesize inductive invariants and adequately strengthen contracts across a large suite of programs. This work is an extended version of a conference paper titled “Invariant Synthesis for Incomplete Verification Engines”.

Sign in / Sign up

Export Citation Format

Share Document