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
Volume13-17-June-2016
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

Other

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

Fingerprint

Automation
Network protocols
Modeling languages
Formal verification

Keywords

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

ASJC Scopus subject areas

  • Software

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 (Vol. 13-17-June-2016, pp. 614-630). Association for Computing Machinery. https://doi.org/10.1145/2908080.2908118

Ivy : Safety verification by interactive generalization. / Padon, Oded; McMillan, Kenneth L.; Panda, Aurojit; Sagiv, Mooly; Shoham, Sharon.

PLDI 2016 - Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. ed. / Chandra Krintz; Emery Berger. Vol. 13-17-June-2016 Association for Computing Machinery, 2016. p. 614-630.

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

Padon, O, McMillan, KL, 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. vol. 13-17-June-2016, Association for Computing Machinery, pp. 614-630, 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, United States, 6/13/16. https://doi.org/10.1145/2908080.2908118
Padon O, McMillan KL, Panda A, Sagiv M, Shoham S. Ivy: Safety verification by interactive generalization. In Krintz C, Berger E, editors, PLDI 2016 - Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. Vol. 13-17-June-2016. Association for Computing Machinery. 2016. p. 614-630 https://doi.org/10.1145/2908080.2908118
Padon, Oded ; McMillan, Kenneth L. ; Panda, Aurojit ; Sagiv, Mooly ; Shoham, Sharon. / Ivy : Safety verification by interactive generalization. PLDI 2016 - Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. editor / Chandra Krintz ; Emery Berger. Vol. 13-17-June-2016 Association for Computing Machinery, 2016. pp. 614-630
@inproceedings{953dae4d52614ce890f5d72a559cfd64,
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",
year = "2016",
month = "6",
day = "2",
doi = "10.1145/2908080.2908118",
language = "English (US)",
volume = "13-17-June-2016",
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",
publisher = "Association for Computing Machinery",

}

TY - GEN

T1 - Ivy

T2 - Safety verification by interactive generalization

AU - Padon, Oded

AU - McMillan, Kenneth L.

AU - Panda, Aurojit

AU - Sagiv, Mooly

AU - Shoham, Sharon

PY - 2016/6/2

Y1 - 2016/6/2

N2 - 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.

AB - 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.

KW - Counterexamples to induction

KW - Distributed systems

KW - Invariant inference

KW - Safety verification

UR - http://www.scopus.com/inward/record.url?scp=84975883211&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84975883211&partnerID=8YFLogxK

U2 - 10.1145/2908080.2908118

DO - 10.1145/2908080.2908118

M3 - Conference contribution

VL - 13-17-June-2016

SP - 614

EP - 630

BT - PLDI 2016 - Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation

A2 - Krintz, Chandra

A2 - Berger, Emery

PB - Association for Computing Machinery

ER -