TY - GEN
T1 - Quantified Invariants via Syntax-Guided Synthesis
AU - Fedyukovich, Grigory
AU - Prabhu, Sumanth
AU - Madhukar, Kumar
AU - Gupta, Aarti
N1 - Publisher Copyright:
© The Author(s). 2019.
PY - 2019
Y1 - 2019
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85069838441&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85069838441&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-25540-4_14
DO - 10.1007/978-3-030-25540-4_14
M3 - Conference contribution
AN - SCOPUS:85069838441
SN - 9783030255398
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 259
EP - 277
BT - Computer Aided Verification - 31st International Conference, CAV 2019, Proceedings
A2 - Dillig, Isil
A2 - Tasiran, Serdar
PB - Springer Verlag
T2 - 31st International Conference on Computer Aided Verification, CAV 2019
Y2 - 15 July 2019 through 18 July 2019
ER -