Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants

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

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

Abstract

We present a new learning algorithm Sorcar to synthesize conjunctive inductive invariants for proving that a program satisfies its assertions. The salient property of this algorithm is that it is property-driven, and for a fixed finite set of n predicates, guarantees convergence in 2n rounds, taking only polynomial time in each round. We implement and evaluate the algorithm and show that its performance is favorable to the existing Houdini algorithm (which is not property-driven) for a class of benchmarks that prove data race freedom of GPU programs and another class that synthesizes invariants for proving separation logic properties for heap manipulating programs.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 26th International Symposium, SAS 2019, Proceedings
EditorsBor-Yuh Evan Chang
PublisherSpringer
Pages323-346
Number of pages24
ISBN (Print)9783030323035
DOIs
StatePublished - Jan 1 2019
Event26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019 - Porto, Portugal
Duration: Oct 8 2019Oct 11 2019

Publication series

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

Conference

Conference26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019
CountryPortugal
CityPorto
Period10/8/1910/11/19

Keywords

  • Conjunctive formulas
  • Horn-ICE learning
  • Invariant synthesis
  • Machine learning

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants'. Together they form a unique fingerprint.

  • Cite this

    Neider, D., Saha, S., Garg, P., & Madhusudan, P. (2019). Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants. In B-Y. E. Chang (Ed.), Static Analysis - 26th International Symposium, SAS 2019, Proceedings (pp. 323-346). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11822 LNCS). Springer. https://doi.org/10.1007/978-3-030-32304-2_16