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

Daniel Neider, P. Madhusudan, Shambwaditya Saha, Pranav Garg, Daejun Park

Research output: Contribution to journalArticlepeer-review

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”.

Original languageEnglish (US)
Pages (from-to)1523-1552
Number of pages30
JournalJournal of Automated Reasoning
Volume64
Issue number7
DOIs
StatePublished - Oct 1 2020

Keywords

  • Incomplete decision procedures
  • Invariant synthesis
  • Machine learning
  • Software verification
  • Undecidable theories

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Fingerprint Dive into the research topics of 'A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines'. Together they form a unique fingerprint.

Cite this