A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines
- PDF / 942,980 Bytes
- 30 Pages / 439.37 x 666.142 pts Page_size
- 3 Downloads / 195 Views
A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines Daniel Neider1 · P. Madhusudan2 · Shambwaditya Saha2 · Pranav Garg3 · Daejun Park2 Received: 22 June 2020 / Accepted: 26 June 2020 © The Author(s) 2020
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”. Keywords Software verification · Invariant synthesis · Undecidable theories · Incomplete decision procedures · Machine learning
B
Daniel Neider [email protected] P. Madhusudan [email protected] Shambwaditya Saha [email protected] Pranav Garg [email protected] Daejun Park [email protected]
1
Max Planck Institute for Software Systems, Kaiserslautern, Germany
2
University of Illinois at Urbana-Champaign, Champaign, IL, USA
3
Amazon Research, New York City, NY, USA
123
D. Neider et al.
1 Introduction The paradigm of deductive verification [24,32] combines manual annotations and semiautomated theorem proving to prove programs correct. Programmers annotate code they develop with contracts and inductive invariants, and use high-level directives to an underlying, mostly-automated logic engine to verify their programs correct. Several mature tools have emerged that support such verification, in particular tools based on the intermediate verification language Boogie [3] and the SMT solver Z3 [18] (e.g., Vcc [13] and Dafny [42]). Viewed through the lens of deductive verification, the primary challenges in automating verification are two-fold. First, even when strong annotations in terms of contracts and inductive invariants are given, the validity problem for the resulting verification conditions is often undecidable (e.g., in reasoning about the heap, reasoning with quantified logics, and reasoning with non-linear arithmetic). Second, the synthesis of loop invariants and strengthenings of contracts that prove a program correct needs to be automated so as to lift this burden cur
Data Loading...
