Automatic Verification of Closures and Lambda-Functions in Python
Viper is a formal verification framework for concurrent object-oriented programs. It is a long-term project in the Chair of Programming Methodology at ETH Zürich. At the core of this infrastructure is the Viper intermediate language, which provides native support for reasoning about the program state using method permissions or ownership, e.g., in the style of separation logic. Improving language expressiveness and implementing advanced language features is currently a high priority of work in our group.
The proposed project is focused on designing and implementing closures and lambda functions in the Viper intermediate language. As an important component of the functional programming paradigm, closures and lambdas (a.k.a. anonymous functions) are essential in a verification language for expressing properties of higher-order algorithms in the same way they are commonly used in imperative programs. This advanced language feature will allow more flexibility for complex specifications and could increase its overall expressiveness.
We propose this project in the context of the Viper’s Python front end, which is currently being developed in our group. The results of this project might be used by our users who develop security-critical software in Python and verify it in Viper. Therefore, we are looking for a motivated Master’s student with conceptual understanding of formal verification, and proficiency in Python is highly advisable.
The design decisions should be based on case studies: one needs to come up with motivational examples which significantly benefit from closures or lambda functions. Such examples could be inspired either by algorithm implementation in functional programming languages, or existing verification tools with support of lambdas, e.g., external page Why3.
One of the main challenges is to find a solution for verifying closures with the presence of captured state which complies with the modular verification approach in Viper. The program on the right illustrates how captured state affects the semantics of closures.
The output is (3, 1, 4, 2), because the state in which the Cell object in build_closure is created is captured by the returned closures. In order to support modularity, the closure factory needs to include the specification of the created closures into its own specification. For more details, read Adding Closure Support to Chalice.
The project could include the following core tasks:
- Finding motivational examples.
- Analyzing pros and cons of existing solutions (based on examples from the previous step).
- Encoding lambda functions in the Viper language.
- Encoding closures with support of captured state.
- Designing the syntax.
- Implementing a Viper-to-Viper translation which decomposes lambda functions into native language primitives and keeps track of source locations for correct error reporting.
The following tasks could extend the project in a successive scenario:
- Justification of the selected design via comparison of different possible encodings in Viper in terms of verification performance, scalability, and automation.
- Comparison analysis of lambdas in Viper and Why3 (based on the same factors).
- Testing closures and lambda functions in combination with other advanced features, such as comprehensions and algebraic datatypes.
If you are interested in this project, please contact Arshavir Ter-Gabrielyan at ETH CAB H-89, or via email: .