Proving Program Equivalence with Constrained Rewriting Induction and Ctrl
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.
Sat 6 Apr Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
|16:00 - 16:30|
|16:30 - 17:00|
|17:00 - 17:30|