Ivy: Safety verification by interactive generalization

Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, Sharon Shoham

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationPLDI 2016 - Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsChandra Krintz, Emery Berger
PublisherAssociation for Computing Machinery
Pages614-630
Number of pages17
ISBN (Electronic)9781450342612
DOIs
StatePublished - Jun 2 2016
Event37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016 - Santa Barbara, United States
Duration: Jun 13 2016Jun 17 2016

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Volume13-17-June-2016

Other

Other37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016
CountryUnited States
CitySanta Barbara
Period6/13/166/17/16

Keywords

  • Counterexamples to induction
  • Distributed systems
  • Invariant inference
  • Safety verification

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Ivy: Safety verification by interactive generalization'. Together they form a unique fingerprint.

  • Cite this

    Padon, O., McMillan, K. L., Panda, A., Sagiv, M., & Shoham, S. (2016). Ivy: Safety verification by interactive generalization. In C. Krintz, & E. Berger (Eds.), PLDI 2016 - Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (pp. 614-630). (Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI); Vol. 13-17-June-2016). Association for Computing Machinery. https://doi.org/10.1145/2908080.2908118