@inproceedings{f804c3381f744933b5ffcfaa974dd8e6,
title = "Ivy: Safety verification by interactive generalization",
abstract = "Despite several decades of research, the problem of formal verification of infinite-state systems has resisted effective automation. We describe a system - Ivy - for interactively verifying safety of infinite-state systems. Ivy's key principle is that whenever verification fails, Ivy graphically displays a concrete counterexample to induction. The user then interactively guides generalization from this counterexample. This process continues until an inductive invariant is found. Ivy searches for universally quantified invariants, and uses a restricted modeling language. This ensures that all verification conditions can be checked algorithmically. All user interactions are performed using graphical models, easing the user's task. We describe our initial experience with verifying several distributed protocols.",
keywords = "Counterexamples to induction, Distributed systems, Invariant inference, Safety verification",
author = "Oded Padon and McMillan, {Kenneth L.} and Aurojit Panda and Mooly Sagiv and Sharon Shoham",
note = "Funding Information: We thank Thomas Ball, Nikolaj Bj{\o}rner, Tej Chajed, Constantin Enea, Neil Immerman, Daniel Jackson, Ranjit Jhala, K. Rustan M. Leino, Giuliano Losa, Bryan Parno, Shaz Qadeer, Zachary Tatlock, James R. Wilcox, the anonymous referees, and the anonymous artifact evaluation referees for insightful comments which improved this paper. Padon, Sagiv, and Shoham were supported by the European Research Council under the European Union's Seventh Framework Program (FP7/2007-2013)/ERC grant agreement no. [321174- VSSC], and by a grant from the Israel Science Foundation (652/11). Panda was supported by a grant from Intel Corporation. Parts of this work were done while Padon and Sagiv were visiting Microsoft Research. Publisher Copyright: {\textcopyright} 2016 ACM.; 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016 ; Conference date: 13-06-2016 Through 17-06-2016",
year = "2016",
month = jun,
day = "2",
doi = "10.1145/2908080.2908118",
language = "English (US)",
series = "Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)",
publisher = "Association for Computing Machinery",
pages = "614--630",
editor = "Chandra Krintz and Emery Berger",
booktitle = "PLDI 2016 - Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation",
}