SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Thu 19 Nov 2020 09:00 - 09:20 at SPLASH-I - R-2 Chair(s): Adrian Sampson, Sheng Chen
Thu 19 Nov 2020 21:00 - 21:20 at SPLASH-I - R-2 Chair(s): Sheng Chen, John Peter Campora

A software analysis is a computer program that takes some representation of a software product as input and produces some useful information about that product as output. A software product line encompasses \emph{many} software product variants, and thus existing analyses can be applied to each of the product variations individually, but not to the entire product line as a whole. Enumerating all product variants and analyzing them one by one is usually intractable due to the combinatorial explosion of the number of product variants with respect to product line features. Several software analyses (e.g., type checkers, model checkers, data flow analyses) have been redesigned/re-implemented to support variability. This usually requires a lot of time and effort, and the variability-aware version of the analysis might have new errors/bugs that do not exist in the original one.

Given an analysis program written in a functional language based on PCF, in this paper we present two approaches to transforming (lifting) it into a semantically equivalent variability-aware analysis. A light-weight approach (referred to as \emph{shallow lifting}) wraps the analysis program into a variability-aware version, exploring all combinations of its input arguments. Deep lifting, on the other hand, is a program rewriting mechanism where the syntactic constructs of the input program are rewritten into their variability-aware counterparts. Compositionally this results in an efficient program semantically equivalent to the input program, modulo variability.

We present the correctness criteria for functional program lifting, together with correctness proof sketches of shallow lifting. We evaluate our approach on a set of program analyses applied to the BusyBox C-language product line.

Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change

09:00 - 10:20
R-2OOPSLA at SPLASH-I +12h
Chair(s): Adrian SampsonCornell University, Sheng ChenUniversity of Louisiana at Lafayette
09:00
20m
Talk
Automatic and Efficient Variability-Aware Lifting of Functional Programs
OOPSLA
Ramy ShahinUniversity of Toronto, Marsha ChechikUniversity of Toronto
Link to publication DOI Pre-print Media Attached
09:20
20m
Talk
Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs
OOPSLA
Alejandro Gómez-LondoñoChalmers University of Technology, Johannes Åman PohjolaData61 at CSIRO / UNSW, Hira Taqdees SyedaChalmers University of Technology, Magnus O. MyreenChalmers University of Technology, Yong Kiam TanCarnegie Mellon University
Link to publication DOI Media Attached
09:40
20m
Talk
Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
OOPSLA
Yiyun LiuUniversity of Maryland at College Park, James ParkerUniversity of Maryland at College Park, Patrick RedmondUniversity of California at Santa Cruz, Lindsey KuperUniversity of California at Santa Cruz, Michael HicksUniversity of Maryland at College Park, Niki VazouIMDEA Software Institute
Link to publication DOI Media Attached
10:00
20m
Talk
Towards a Formal Foundation of Intermittent Computing
OOPSLA
Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University
Link to publication DOI Media Attached
21:00 - 22:20
R-2OOPSLA at SPLASH-I
Chair(s): Sheng ChenUniversity of Louisiana at Lafayette, John Peter CamporaUniversity of Louisiana at Lafayette
21:00
20m
Talk
Automatic and Efficient Variability-Aware Lifting of Functional Programs
OOPSLA
Ramy ShahinUniversity of Toronto, Marsha ChechikUniversity of Toronto
Link to publication DOI Pre-print Media Attached
21:20
20m
Talk
Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs
OOPSLA
Alejandro Gómez-LondoñoChalmers University of Technology, Johannes Åman PohjolaData61 at CSIRO / UNSW, Hira Taqdees SyedaChalmers University of Technology, Magnus O. MyreenChalmers University of Technology, Yong Kiam TanCarnegie Mellon University
Link to publication DOI Media Attached
21:40
20m
Talk
Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
OOPSLA
Yiyun LiuUniversity of Maryland at College Park, James ParkerUniversity of Maryland at College Park, Patrick RedmondUniversity of California at Santa Cruz, Lindsey KuperUniversity of California at Santa Cruz, Michael HicksUniversity of Maryland at College Park, Niki VazouIMDEA Software Institute
Link to publication DOI Media Attached
22:00
20m
Talk
Towards a Formal Foundation of Intermittent Computing
OOPSLA
Milijana SurbatovichCarnegie Mellon University, Brandon LuciaCarnegie Mellon University, Limin JiaCarnegie Mellon University
Link to publication DOI Media Attached