Proving Program Equivalence with Constrained Rewriting Induction and Ctrl (PERR 2019 - 3rd Workshop on Program Equivalence and Relational Reasoning)

Sat 6 - Thu 11 April 2019 Prague, Czech Republic

Who

Carsten Fuhs, Cynthia Kop, Naoki Nishida

Track

PERR 2019

Time Zone

The program is currently displayed in (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Sat 6 Apr 2019 16:30 - 17:00 at S1 (PERR) - IV

Abstract

We prove equivalence of imperative programs by an automatic conversion of the functions in the input program to an equivalent Logically Constrained Term Rewrite System (LCTRS), followed by constrained rewriting induction (either fully automatically or guided by the user) to analyze equivalence of the corresponding functions in the LCTRS. Our approach is implemented in the tool Ctrl.

Carsten Fuhs

Birkbeck, University of London

United Kingdom

Cynthia Kop

Radboud University Nijmegen

Netherlands

Naoki Nishida

Nagoya University

Japan