[pl-seminar] Yotam Feldman talk starting *now* in 4310 CS

[Ben Liblit <liblit@xxxxxxxxxxx>]

Yotam Feldman's PL seminar talk is starting *now* in 4310 CS.  Go go go!

--- Begin Message ---

Date:	Mon, 20 Aug 2018 18:49:00 +0000
From:	Thomas Reps <reps@xxxxxxxxxxx>
Subject:	[pl-seminar] Yotam Feldman talk, Thursday, 11-noon in 4310 CS

Hi,

 

Yotam Feldman is visiting this week from Tel-Aviv University, where he works with Mooly Sagiv and Sharon Shoham.  I’ve scheduled his talk for Thursday, 11-noon in 4310 CS.  I apologize for scheduling it in the morning, but because Thursday is his last day, I wanted there to be some time for him to meet with people before he departs.

 

Tom

==========================================================================================================

 

Title: Inferring Phase Invariants from Phase Sketches

Speaker: Yotam Feldman

Thursday, Aug. 23, 2018

11:00 am - noon

Infinite state systems such as distributed protocols are challenging to verify using interactive theorem provers or automatic verification tools. Of these techniques, deductive verification is highly expressive but requires the user to annotate the system with inductive invariants. Even if the rest of the proof is automatically checked, inductive invariants are challenging to find, even for experts, who must often go through many iterations before successfully proving safety. Thus, to further increase automation, one might hope to instead automatically infer the necessary invariants, but existing invariant inference techniques are unreliable and opaque. For example, inference may diverge or run for so long as to be useless; furthermore, feedback to the user tends to be all-or-nothing, either finding a full invariant to prove safety or reporting that no invariant could be found. In such cases, the user is left to tweak the system using trial and error with little guidance until inference manages to succeed, or to try directly annotating the system with invariants until safety is proved.

In this work, we propose user-guided invariant inference based on phase invariants, an automaton structure that captures the different logical phases of the protocol. The automaton's states are labeled with assertions that hold in that phase, while edges between phases correspond to atomic transitions of the protocol. The user conveys their intuition by specifying a phase sketch, which is a partially labeled (or completely unlabeled) automaton, from which a full labeling is inferred automatically. The sketch provides guidance to the inference procedure about how to find an invariant than would otherwise be available; as a result, the user obtains more reliable and transparent results.

We demonstrate the utility of this approach by analyzing several distributed protocols from the literature using phase invariants. Our results show that the additional structure from phase sketches can accelerate the process of inferring an invariant to prove safety. We find that phase sketches are pleasantly well matched to the intuitive reasoning routinely used by domain experts to understand why distributed protocols are correct, so that providing a phase sketch reuses this existing intuition.

Work in progress jointly with James R. Wilcox, Sharon Shoham and Mooly Sagiv.

 

 

_______________________________________________
Pl-seminar mailing list
Pl-seminar@xxxxxxxxxxx
https://lists.cs.wisc.edu/mailman/listinfo/pl-seminar

--- End Message ---