Skip to main content

Quantified Invariants via Syntax-Guided Synthesis

Author(s): Fedyukovich, Grigory; Prabhu, Sumanth; Madhukar, Kumar; Gupta, Aarti

To refer to this page use:
Abstract: Programs with arrays are ubiquitous. Automated reasoning about arrays necessitates discovering properties about ranges of elements at certain program points. Such properties are formally specified by universally quantified formulas, which are difficult to find, and difficult to prove inductive. In this paper, we propose an algorithm based on an enumerative search that discovers quantified invariants in stages. First, by exploiting the program syntax, it identifies ranges of elements accessed in each loop. Second, it identifies potentially useful facts about individual elements and generalizes them to hypotheses about entire ranges. Finally, by applying recent advances of SMT solving, the algorithm filters out wrong hypotheses. The combination of properties is often enough to prove that the program meets a safety specification. The algorithm has been implemented in a solver for Constrained Horn Clauses, Freq-Horn, and extended to deal with multiple (possibly nested) loops. We show that FreqHorn advances state-of-the-art on a wide range of public array-handling programs.
Publication Date: 2019
Citation: Fedyukovich, Grigory, Sumanth Prabhu, Kumar Madhukar, and Aarti Gupta. "Quantified Invariants via Syntax-Guided Synthesis." In International Conference on Computer Aided Verification (2019): pp. 259-277. doi:10.1007/978-3-030-25540-4_14
DOI: 10.1007/978-3-030-25540-4_14
ISSN: 0302-9743
EISSN: 1611-3349
Pages: 259 - 277
Type of Material: Conference Article
Journal/Proceeding Title: International Conference on Computer Aided Verification
Version: Final published version. This is an open access article.

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.