• You are, of course, free to suggest your own project and discuss it with us.

• To ensure that everyone knows what they should do and we know what you are actually doing, you will submit a short (about 1-2 pages) proposal for the project you decide on. This should include e.g. deliverables in terms of code or algorithms, a plan of attack for your problem, more background references, examples, etc. Deadline is Thursday, April 13.

• Projects from our list of suggestions will be assigned on a first-come-first-served basis, so don't wait until the last minute to have a look. If you picked a project, send an announcement over Moodle so that everyone knows.

• You can work on these projects in groups of up to two people.

The name after each project title indicate the contact person for the project.

1. Extend Stainless' alias analysis procedure [Nicolas]
2. Build an Inox frontend with type inferrence [Romain]
3. Build a Sledgehammer-like extension for Stainless [Nicolas]
4. SMT-solver quantifiers backend in Inox [Nicolas]
5. Explore proof tactics in Welder [Romain]
6. Extend the dotty VS code plugin with support for Stainless [Nicolas]
7. Benchmark (and improve) the Stainless pipeline performance [Nicolas and Georg]
8. JS frontend for Stainless [Nicolas]

Stainless supports verification of certain imperative constructs under some aliasing restrictions. The goal of this project would be to precisely define these restrictions and implement some new analysis that allow more complex cases on non-aliasing.

The Inox solver is targeted towards Scala verification and can verify Scala code through the Stainless frontend. However, using the Inox solver directly can be complicated and unintuitive due to the complexity of constructing the Inox expressions. A new parser is being developed in order to simplify this process. This project should extend this parser to parse complete programs and could form the basis of a new (and faster) Stainless frontend for simple programs.

In the presence of many lemmas and axioms, verification can become bogged down and very slow. However, proving more complex properties requires the definition of more intermediate lemmas. This project should focus on finding good heuristics to enable scalable automated verification in the presence of many lemmas.

See http://isabelle.in.tum.de/website-Isabelle2009-1/sledgehammer.html for inspiration.

Another useful direction would consist in supporting certain proof helpers such as because and by that can provide more control over which lemmas are used to prove a property.

The Inox solver is good at finding counterexamples, however this property is not always useful and can be detrimental to verification capabilities of the system. The SMT solvers that underly Inox' reasoning abilities provide support for quantified propositions. The goal of this project would be to provide a (semantic preserving) encoding for the full Inox language using these quantifiers.

As you have seen, constructing even simple inductive proofs in Welder can take a lot of repetitive work. In certain cases, it should be possible to identify proof strategies through formula introspection. The goal of this project is to identify such cases and provide a few automated proof strategies to simplify the verification of these cases.

The full Stainless verification pipeline starts from scratch at each invocation. Building on the recent VS code plugin for dotty https://github.com/smarter/vscode-dotty, provide IDE support for the Stainless system.

Alternatively, ensure the scala compiler plugin upon which Stainless is based can be used in an incremental manner (and an SBT plugin would be nice too!)

Benchmark the Stainless translation pipeline that takes Scala code and transpiles it down to Inox expressions. After identifying the major bottle-necks, consider which optimizations you could propose in the pipeline to improve its performance.

Provide a Javascript frontend for Stainless based on the recent extension with support for Any and complex subtyping.