Squeezing arrays for fun and profit — Verification of unbounded loops with inductive rank reduction
Date: Thursday, February 20, 2020
Time: 11:00 AM to 12:00 PM Note: all times are in the Eastern Time Zone
Location: Hewlett Room, 32-G882
Event Type: Seminar
Room Description: Hewlett Room, 32-G882
Host: Daniel Jackson
Contact: Mark J. Pearrow, email@example.com
Speaker URL: None
TALK: Squeezing arrays for fun and profit — Verification of unbounded loops with inductive rank reduction
Joint work with Oren Ish-Shalom, Noam Rinetzky, Sharon Shoham
Automatic verification of array manipulating programs is a challenging problem because it often amounts to the inference of inductive quantified loop invariants which, in some cases, may not even be first-order expressible. In this talk I will present an alternative approach, inductive rank reduction, which uses a different inductive scheme based on the size of the array. While we have used it for array programs, taking advantage of highly mature array property fragment decision procedure in Z3, the theoretical framework applies to any data structure whose “rank” (typically size) can be expressed.
We employ a “squeezer”, a function that converts a program state σ with an array of length r to a smaller state σ' with an array of length r-1. Then we use reasoning by induction, proving that if σ’ is safe then so is σ. The induction step is carried out using a simulation arguments correlating traces whose states have ranks r and r-1.
This way it is both fun and profitable.
Created by Mark J. Pearrow at Tuesday, February 18, 2020 at 10:28 AM.