The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Ivy: safety verification by interactive generalization
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
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.
How it got here
How it got here
agent via openalex
Added
2026-10-25 17:24 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@misc{padon2016ivy,
title = {Ivy: safety verification by interactive generalization},
author = {Oded Padon and Kenneth L. McMillan and Aurojit Panda and Mooly Sagiv and Sharon Shoham},
year = {2016},
journal = {Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation},
pages = {614--630},
doi = {10.1145/2908080.2908118},
}