@inproceedings{1e5729f1c4944d52b8477dcaf1995107,
title = "Sorcar: Property-Driven Algorithms for Learning Conjunctive Invariants",
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.",
keywords = "Conjunctive formulas, Horn-ICE learning, Invariant synthesis, Machine learning",
author = "Daniel Neider and Shambwaditya Saha and Pranav Garg and P. Madhusudan",
note = "Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2019.; 26th International Static Analysis Symposium, SAS 2019 held as part of the 3rd World Congress on Formal Methods, FM 2019 ; Conference date: 08-10-2019 Through 11-10-2019",
year = "2019",
doi = "10.1007/978-3-030-32304-2_16",
language = "English (US)",
isbn = "9783030323035",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "323--346",
editor = "Chang, {Bor-Yuh Evan}",
booktitle = "Static Analysis - 26th International Symposium, SAS 2019, Proceedings",
address = "Germany",
}