SynRG: Syntax Guided Synthesis of Invariants with Alternating Quantifiers.
Elizabeth Polgreen, Sanjit A. Seshia · arXiv (Cornell University) · 2020
Proving properties of systems frequently requires the user to provide hand-written invariants and pre- and post-conditions. A~significant body of work exists attempting to automate the generation of loop invariants in code, but the state of the art cannot yet tackle the combination of quantifiers and potentially unbounded data structures. We present SynRG, a synthesis algorithm based on restricting the synthesis problem to generate candidate solutions with quantification over a finite domain, and then generalizing these candidate solutions to the unrestricted domain of the original specification. We give an exemplar of our method that generates invariants with quantifiers over array indices. Our algorithm is, in principle, able to synthesize predicates with arbitrarily many levels of alternating quantification. We report experiments that require invariants with one alternation that are already out of reach of all existing solvers.