English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Paper

Invariant Synthesis for Incomplete Verification Engines

MPS-Authors
/persons/resource/persons215577

Neider,  Daniel
Group R. Majumdar, Max Planck Institute for Software Systems, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

arXiv:1712.05581.pdf
(Preprint), 664KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Neider, D., Garg, P., Madhusudan, P., Saha, S., & Park, D. (2017). Invariant Synthesis for Incomplete Verification Engines. Retrieved from http://arxiv.org/abs/1712.05581.


Cite as: https://hdl.handle.net/21.11116/0000-0000-7650-1
Abstract
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.