ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sat 6 Apr 2019 16:30 - 17:00 at S1 (PERR) - IV

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 - 18:00: PERR - IV at S1 (PERR)
perr-2019-papers16:00 - 16:30
Moritz Kiefer, Mattias UlbrichKarlsruhe Institute of Technology
perr-2019-papers16:30 - 17:00
Carsten FuhsBirkbeck, University of London, Cynthia KopRadboud University Nijmegen, Naoki NishidaNagoya University
perr-2019-papers17:00 - 17:30
Stefan CiobacaAlexandru Ioan Cuza University of Iasi, Dorel Lucanu, Sebastian Buruiana