REFINITY to Model and Prove Program Transformation Rules (APLAS 2020 - Research Papers)

Write a Blog >>

Mon 30 November - Wed 2 December 2020

Track

APLAS 2020 Research Papers

Time Zone

The program is currently displayed in (GMT+09:00) Osaka, Sapporo, Tokyo.

Use conference time zone: (GMT+09:00) Osaka, Sapporo, TokyoSelect 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

Wed 2 Dec 2020 16:30 - 17:00 at online - Synthesis and Program Transformation Chair(s): Cristina David

Abstract

REFINITY is a workbench for modeling statement-level transformation rules on Java programs with the aim to formally verify their correctness. It is based on Abstract Execution, a verification framework for abstract programs with a high degree of proof automation, and interfaces to the KeY program prover. We describe user interface and functionality of REFINITY, and illustrate its capabilities along the application to proving conditional correctness of a code refactoring rule.

Time Zone

The program is currently displayed in (GMT+09:00) Osaka, Sapporo, Tokyo.

Use conference time zone: (GMT+09:00) Osaka, Sapporo, TokyoSelect other time zone

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

Time Band

Display full programSpecify a time band

Save

Session Program

Wed 2 Dec
Displayed time zone: Osaka, Sapporo, Tokyo change

15:30 - 17:00	Synthesis and Program TransformationResearch Papers at online Chair(s): Cristina David University of Oxford

15:30 30m Talk		Relational Synthesis for Pattern Matching Research Papers Dmitrii Kosarev , Dmitri Boulytchev Saint Petersburg State University / JetBrains Research
16:00 30m Talk		Parameterized Synthesis with Safety Properties Research Papers Oliver Markgraf Technische Universität Kaiserslautern, Anthony Widjaja Lin Technische Universität Kaiserslautern, Daniel Neider Max Planck Institute for Software Systems, Muhammad Najib Technische Universität Kaiserslautern, Chih-Duo Hong University of Oxford
16:30 30m Talk		REFINITY to Model and Prove Program Transformation Rules Research Papers Dominic Steinhöfel Technical University of Darmstadt

REFINITY to Model and Prove Program Transformation Rules

Program Display Configuration

Program Display Configuration

Wed 2 DecDisplayed time zone: Osaka, Sapporo, Tokyo change

Dominic Steinhöfel

Technical University of Darmstadt

Wed 2 Dec
Displayed time zone: Osaka, Sapporo, Tokyo change