A data driven approach for algebraic loop invariants

Rahul Sharma, Saurabh Gupta, Bharath Hariharan, Alex Aiken, Percy Liang, Aditya V. Nori

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

Abstract

We describe a Guess-and-Check algorithm for computing algebraic equation invariants of the form Λi fi (x1,..., xn) = 0, where each fi is a polynomial over the variables x1,...,x n of the program. The "guess" phase is data driven and derives a candidate invariant from data generated from concrete executions of the program. This candidate invariant is subsequently validated in a "check" phase by an off-the-shelf SMT solver. Iterating between the two phases leads to a sound algorithm. Moreover, we are able to prove a bound on the number of decision procedure queries which Guess-and-Check requires to obtain a sound invariant. We show how Guess-and-Check can be extended to generate arbitrary boolean combinations of linear equalities as invariants, which enables us to generate expressive invariants to be consumed by tools that cannot handle non-linear arithmetic. We have evaluated our technique on a number of benchmark programs from recent papers on invariant generation. Our results are encouraging - we are able to efficiently compute algebraic invariants in all cases, with only a few tests.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Proceedings
Pages574-592
Number of pages19
DOIs
StatePublished - 2013
Externally publishedYes
Event22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013 - Rome, Italy
Duration: Mar 16 2013Mar 24 2013

Publication series

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

Conference

Conference22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013
Country/TerritoryItaly
CityRome
Period3/16/133/24/13

Keywords

  • Non-linear
  • SMT
  • loop invariants

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'A data driven approach for algebraic loop invariants'. Together they form a unique fingerprint.

Cite this