Thursday, August 11th

View this program: with abstractssession overviewtalk overviewside by side with other conferences

08:30-09:00Coffee & Refreshments
09:30-10:30 Session 124B: Keynote Talk

Title: Regression verification of unbalanced recursive functions with multiple calls

Speaker:  Chaked R.J.Sayedoff  and Ofer Strichman ,  Technion, Israel

Abstract: Given two programs p1 and p2, typically two versions of the sameprogram, the goal of \emph{regression verification} is to mark pairs offunctions from p1 and p2 that are equivalent, given a definitionof equivalence. The most common definition is that of \emph{partialequivalence}, namely that the two functions emit the same output if theyare fed with the same input and they both terminate. The strategy usedby the Regression Verification Tool (RVT) is to progress bottom up onthe call graphs of P1,P2, abstract those functions that were alreadyproven to be equivalent with uninterpreted functions, turn loops intorecursion, and abstract the recursive calls also with uninterpretedfunctions. This enables it to create verification conditions in the formof small programs that are loop- and recursion-free. This method workswell for recursive functions as long as they are in sync, and typicallyfails otherwise. In this work we study the problem of provingequivalence when the two recursive functions are not in sync.Effectively we extend  previous work that studied this problem forfunctions with a single recursive call site, to the general case. Wealso introduce a method for detecting automatically the unrolling thatis necessary for making two recursive functions synchronize, whenpossible. We show examples of pairs of functions with multiple recursivecalls that can now be proven equivalent with our method, but cannot beproven equivalent with any other automated verification system.

Location: Ullmann 305
Regression verification of unbalanced recursive functions with multiple calls (abstract)
10:30-11:00Coffee Break
11:00-12:30 Session 125L: Research Papers
Location: Ullmann 305
Compositional Approaches to Games in Model Checking (abstract)
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques (Extended Abstract) (abstract)
Extending a Lemma Generation Approach for Rewriting Induction on Logically Constrained Term Rewriting Systems (abstract)
PRESENTER: Kasper Hagens
12:30-14:00Lunch Break

Lunches will be held in Taub hall and in The Grand Water Research Institute.

14:00-15:00 Session 127L: Research Papers
Location: Ullmann 305
Implementing a Path Based Equivalence Checker for Petri net based Models of Programs (abstract)
Generating Mutation Tests Using an Equivalence Prover (abstract)
15:30-16:00Coffee Break
16:00-17:00 Session 131J: Invited Talk

Title: Compositional relational reasoning via operational game semantics

Andrzej Murawski (University of Oxford)

Abstract: We use operational game models as a guide to develop relational techniques for establishing contextual equivalences with respect to contexts drawn from a hierarchy of four call-by-value higher-order languages,with either general or ground-type references and with either call/cc or no control operator. In game semantics, the differences between the contexts can be captured by the absence or presence of the O-visibility and O-bracketing conditions.

The proposed technique, which we call Kripke Normal-Form Bisimulations, combines insights from normal-form bisimulation and Kripke-style logical relations with game semantics. In particular, the role of the heap is abstracted away using Kripke-style world transition systems. The differences between the four kinds of contexts manifest themselves through simple local conditions that can be shown to correspond to O-visibility and O-bracketing, where applicable.

The technique is sound and complete by virtue of correspondence with operational game semantics. Moreover, the framework developed in the paper sheds a new light on other related developments, such as backtracking and private transitions in Kripke logical relations, which can be related to specific phenomena in game models.


This is joint work with Guilhem Jaber (Universite de Nantes).


Location: Ullmann 305
Compositional relational reasoning via operational game semantics (abstract)
18:00-19:30Workshop Dinner (at the Technion, Taub Terrace Floor 2) - Paid event