Verification as learning geometric concepts

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

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

Abstract

We formalize the problem of program verification as a learning problem, showing that invariants in program verification can be regarded as geometric concepts in machine learning. Safety properties define bad states: states a program should not reach. Program verification explains why a program's set of reachable states is disjoint from the set of bad states. In Hoare Logic, these explanations are predicates that form inductive assertions. Using samples for reachable and bad states and by applying well known machine learning algorithms for classification, we are able to generate inductive assertions. By relaxing the search for an exact proof to classifiers, we obtain complexity theoretic improvements. Further, we extend the learning algorithm to obtain a sound procedure that can generate proofs containing invariants that are arbitrary boolean combinations of polynomial inequalities. We have evaluated our approach on a number of challenging benchmarks and the results are promising.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 20th International Symposium, SAS 2013, Proceedings
Pages388-411
Number of pages24
DOIs
StatePublished - Sep 26 2013
Externally publishedYes
Event20th International Static Analysis Symposium, SAS 2013 - Seattle, WA, United States
Duration: Jun 20 2013Jun 22 2013

Publication series

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

Other

Other20th International Static Analysis Symposium, SAS 2013
CountryUnited States
CitySeattle, WA
Period6/20/136/22/13

Keywords

  • loop invariants
  • machine learning
  • verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Verification as learning geometric concepts'. Together they form a unique fingerprint.

Cite this