TY - GEN
T1 - Invariant synthesis for incomplete verification engines
AU - Neider, Daniel
AU - Garg, Pranav
AU - Madhusudan, P.
AU - Saha, Shambwaditya
AU - Park, Daejun
N1 - Publisher Copyright:
© The Author(s) 2018.
PY - 2018
Y1 - 2018
N2 - We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counter-example guided inductive synthesis principle (CEGIS) and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates. Moreover, we evaluate our framework in two verification settings, one in which verification engines need to handle quantified formulas and one in which verification engines have to reason about heap properties expressed in an expressive but undecidable separation logic. Our experiments show that our invariant synthesis framework based on non-provability information can both effectively synthesize inductive invariants and adequately strengthen contracts across a large suite of programs.
AB - We propose a framework for synthesizing inductive invariants for incomplete verification engines, which soundly reduce logical problems in undecidable theories to decidable theories. Our framework is based on the counter-example guided inductive synthesis principle (CEGIS) and allows verification engines to communicate non-provability information to guide invariant synthesis. We show precisely how the verification engine can compute such non-provability information and how to build effective learning algorithms when invariants are expressed as Boolean combinations of a fixed set of predicates. Moreover, we evaluate our framework in two verification settings, one in which verification engines need to handle quantified formulas and one in which verification engines have to reason about heap properties expressed in an expressive but undecidable separation logic. Our experiments show that our invariant synthesis framework based on non-provability information can both effectively synthesize inductive invariants and adequately strengthen contracts across a large suite of programs.
UR - http://www.scopus.com/inward/record.url?scp=85045852045&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85045852045&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-89960-2_13
DO - 10.1007/978-3-319-89960-2_13
M3 - Conference contribution
AN - SCOPUS:85045852045
SN - 9783319899596
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 232
EP - 250
BT - Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings
A2 - Beyer, Dirk
A2 - Huisman, Marieke
PB - Springer
T2 - 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018
Y2 - 14 April 2018 through 20 April 2018
ER -