Ivy: Safety verification by interactive generalization

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

Research output: Contribution to journalArticlepeer-review

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)
Pages (from-to)614-630
Number of pages17
JournalACM SIGPLAN Notices
Volume51
Issue number6
DOIs
StatePublished - Jun 2016

Keywords

  • counterexamples to induction
  • distributed systems
  • invariant inference
  • safety verification

ASJC Scopus subject areas

  • General Computer Science

Fingerprint

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

Cite this