Verifying Context Oriented Programs With Refinement Types

Описание: Master thesis presentation by Sebastian Lemus

Title: Verifying Context Oriented Programs With Refinement Types

Abstract: Context-Oriented Programming (COP) is a paradigm intended for writing software that has the ability to adapt its behavior in response to a given execution context. It does so by providing a (de)activation mechanism that dynamically declares the scope of a given functionality, depending on the properties of the data supplied by the context. Though this way of writing programs may enhance modularity and expressivity, it also poses some challenges when validating the execution of the program. Testing a COP program requires the programmer to reason about the immense space of possible state values, and how those affect the flow of the program by identifying the components that are activated or deactivated at a given point in time. There is an ongoing research effort to create tools and frameworks to improve the correctness of COP programs, however, no usage of Software Verification tools have been found to date on this area. This case study aims to illustrate how to reason about COP programs using Refinement Types, focusing the formulation of properties regarding the interactions between active components. The result of this study is a verified graphical editor application that is used to assess the integration of COP abstractions with Refinement Types as a valid and useful approach.

Term: 2025-10
Promotor: Nicolas Cardozo

#FLAGlab #pil