Invariant synthesis for incomplete verification engines

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 counter-example guided inductive synthesis principle (CEGIS) 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.

Original languageEnglish (US)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings
EditorsDirk Beyer, Marieke Huisman
PublisherSpringer
Pages232-250
Number of pages19
ISBN (Print)9783319899596
DOIs
StatePublished - 2018
Event24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018 - Thessaloniki, Greece
Duration: Apr 14 2018Apr 20 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10805 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018
Country/TerritoryGreece
CityThessaloniki
Period4/14/184/20/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Invariant synthesis for incomplete verification engines'. Together they form a unique fingerprint.

Cite this