Fri 17 Jun 2016 09:30 - 10:00 at Grand Ballroom San Rafael - Verification II Chair(s): Armando Solar-Lezama

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.

Fri 17 Jun
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

09:00 - 10:00: Research Papers - Verification II at Grand Ballroom San Rafael
Chair(s): Armando Solar-LezamaMIT
pldi-2016-papers09:00 - 09:30
Nikolaj BjørnerMicrosoft Research, Klaus GleissenthallTechnische Universität München, Andrey RybalchenkoMicrosoft Research
Media Attached
pldi-2016-papers09:30 - 10:00
Oded PadonTel Aviv University, Kenneth L. McMillanMicrosoft Research, Aurojit Panda, Mooly SagivTel Aviv University, Sharon Shoham
Media Attached