Skip to main content

Quantified Invariants via Syntax-Guided Synthesis

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

Download
To refer to this page use: http://arks.princeton.edu/ark:/88435/pr1mj9q
Full metadata record
DC FieldValueLanguage
dc.contributor.authorFedyukovich, Grigory-
dc.contributor.authorPrabhu, Sumanth-
dc.contributor.authorMadhukar, Kumar-
dc.contributor.authorGupta, Aarti-
dc.date.accessioned2021-10-08T19:46:41Z-
dc.date.available2021-10-08T19:46:41Z-
dc.date.issued2019en_US
dc.identifier.citationFedyukovich, 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_14en_US
dc.identifier.issn0302-9743-
dc.identifier.urihttp://arks.princeton.edu/ark:/88435/pr1mj9q-
dc.description.abstractPrograms 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.en_US
dc.format.extent259 - 277en_US
dc.language.isoen_USen_US
dc.relation.ispartofInternational Conference on Computer Aided Verificationen_US
dc.rightsFinal published version. This is an open access article.en_US
dc.titleQuantified Invariants via Syntax-Guided Synthesisen_US
dc.typeConference Articleen_US
dc.identifier.doi10.1007/978-3-030-25540-4_14-
dc.identifier.eissn1611-3349-
pu.type.symplectichttp://www.symplectic.co.uk/publications/atom-terms/1.0/conference-proceedingen_US

Files in This Item:
File Description SizeFormat 
QuantifiedInvariantsSyntaxGuidedSynthesis.pdf632.09 kBAdobe PDFView/Download


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