Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
projects [2016/11/15 17:06] vkuncak |
projects [2017/04/11 11:43] vkuncak |
||
|---|---|---|---|
| Line 13: | Line 13: | ||
| Below we list several projects reflecting the current interests of our research group. All projects can be adapted to fit the scope of a semester project (bachelor & master) or master's project. | Below we list several projects reflecting the current interests of our research group. All projects can be adapted to fit the scope of a semester project (bachelor & master) or master's project. | ||
| - | Many of these project are based on the [[http://lara.epfl.ch/w/leon|Leon system]] for synthesis and verification. We suggest that you get the basic idea of Leon in any case. Please note that we release software under open source licenses and we request our contributors to agree that EPFL LARA holds copyright of the code that you contribute. | + | Many of these project are based on the [[http://lara.epfl.ch/w/leon|Leon system]] for synthesis and verification. We suggest that you get the basic idea of Leon in any case. |
| + | |||
| + | **Licence for code:** Please note that we release software under open source licenses and we request our contributors to agree that EPFL LARA holds copyright of the code that you contribute. | ||
| **Disclaimer:** If you have your own idea, feel free to check with us, but please note that we some times cannot accommodate your own project suggestions even if the student is brilliant and the project is excellent. Moreover, even if you select one of the projects listed below, we reserve the right to not offer you the project. By deciding to talk to us you agree that you will not require detailed justification on why we made our negative decision. | **Disclaimer:** If you have your own idea, feel free to check with us, but please note that we some times cannot accommodate your own project suggestions even if the student is brilliant and the project is excellent. Moreover, even if you select one of the projects listed below, we reserve the right to not offer you the project. By deciding to talk to us you agree that you will not require detailed justification on why we made our negative decision. | ||
| Line 24: | Line 26: | ||
| The goal of this task is to design a reasonably fast front end for the subset of Scala that is relevant for Leon. The front-end should be able to process existing regression test suite for Leon, but will necessarily deviate from scalac or dotty on some examples. In particular, the type system can be simpler and implicit resolution can be more restrictive than in Scala. Optionally, the front end may support omitting type declarations even for certain function parameters, if these can be inferred given a whole program using type inference for parametric types with simple structural subtyping. | The goal of this task is to design a reasonably fast front end for the subset of Scala that is relevant for Leon. The front-end should be able to process existing regression test suite for Leon, but will necessarily deviate from scalac or dotty on some examples. In particular, the type system can be simpler and implicit resolution can be more restrictive than in Scala. Optionally, the front end may support omitting type declarations even for certain function parameters, if these can be inferred given a whole program using type inference for parametric types with simple structural subtyping. | ||
| + | |||
| + | === Verifying JavaScript === | ||
| + | |||
| + | Design a translation of a clean subset of JavaScript including higher-order functions and (mostly immutable) objects into Leon. Map numbers into Double (apply overflow checks as needed), and enable annotations or special function calls to describe types and contracts. | ||
| + | |||
| + | Note that `(f:TObj) => e` can be encoded as `TObj(x => e)`. | ||
| + | |||
| + | === AST-Based Version Control === | ||
| + | |||
| + | Develop a layer on top of git for managing revisions of Leon programs at the level of high-level syntax tree transformations, with conflict resolution doing semantic commutativity checks. | ||
| === Easily editable and exportable hand-writing presentation videos === | === Easily editable and exportable hand-writing presentation videos === | ||
| Line 60: | Line 72: | ||
| This project likely requires the previous project on parameterized-length bitvectors. | This project likely requires the previous project on parameterized-length bitvectors. | ||
| - | === Verify Electronic Contract Code === | + | === Verify Smart Contract Code === |
| Verify correctness of electronic contract code. See, for example: | Verify correctness of electronic contract code. See, for example: | ||