SPLASH 2014
Mon 20 - Fri 24 October 2014 Portland, Oregon, United States
Mon 20 Oct 2014 10:30 - 11:00 at Salon G - Research Papers Chair(s): Marco Servetto

Abstract: Often when programmers modify source code they intend to preserve some parts of the program behaviour. We propose a formal criterion by which to characterise the preserved part of the program behaviour. Two program versions are equivalent up to a set of affected objects A, if executions of the two versions correspond at each execution step when we do not consider the objects in A. We propose a sufficient condition for this criterion. It suffices to establish that traces of method calls and returns between A objects and other objects are equivalent. Examining the stack and heap at each execution step is not necessary. We give a proof of the sufficiency of this condition, much of which we have automatically verified using Dafny. We also discuss our experiences with Dafny and detail how some interesting parts of our Dafny proof work.

Mon 20 Oct

Displayed time zone: Tijuana, Baja California change

10:30 - 12:00
Research PapersFOOL at Salon G
Chair(s): Marco Servetto Victoria University of Wellington
10:30
30m
Talk
Program Equivalence through Trace Equivalence
FOOL
Tim Wood Imperial College, Sophia Drossopoulou Imperial College London
File Attached
11:00
30m
Talk
The Problem of Structural Type Tests in a Gradual-Typed Language
FOOL
John Boyland University of Wisconsin, Milwaukee
File Attached
11:30
30m
Talk
Managing Gradual Typing with Message-Safety in Dart
FOOL
File Attached