Squeezing arrays for fun and profit — Verification of unbounded loops with inductive rank reduction

Speaker: Shachar Itzhaky , Technion

Date: Thursday, February 20, 2020

Time: 11:00 AM to 12:00 PM Note: all times are in the Eastern Time Zone

Public: Yes

Location: Hewlett Room, 32-G882

Event Type: Seminar

Room Description: Hewlett Room, 32-G882

Host: Daniel Jackson

Contact: Mark J. Pearrow, dnj@csail.mit.edu

Relevant URL:

Speaker URL: None

Speaker Photo:
None

Reminders to: seminars@csail.mit.edu

Reminder Subject: 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.

Research Areas:

Impact Areas:

This event is not part of a series.

Created by Mark J. Pearrow Email at Tuesday, February 18, 2020 at 10:28 AM.