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 [2018/08/22 14:45] vkuncak |
projects [2019/12/16 15:47] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Available Student Projects in LARA - EPFL Internal Page ====== | ====== Available Student Projects in LARA - EPFL Internal Page ====== | ||
| - | **(c) 2016-2018 Laboratory for Automated Reasoning and Analysis. All Rights Reserved. Any reproduction of the parts of this page in printed or electronic form requires a prior written permission from Viktor Kuncak.** | + | **(c) 2016-2018 Laboratory for Automated Reasoning and Analysis. All Rights Reserved. Any reproduction of the parts of this page in printed or electronic form requires a prior written permission from Viktor Kunčak.** |
| - | These projects are suitable for both **BSc** and **MSc** projects (including **master's thesis** projects) for students in the **IC school** of **EPFL**, and are suitable for both **computer science** and **communication systems** students. Each project is for **one student** in a given semester. Students report directly to [[http://lara.epfl.ch/~kuncak|Prof. Viktor Kuncak]], even if PhD students are involved to help with various aspects of the project. The information on whether the project is available or not is also maintained only by Viktor Kuncak, so please contact him if you are interested in the project. | + | These projects are suitable for both **BSc** and **MSc** projects (including **master's thesis** projects) for students in the **IC school** of **EPFL**, and are suitable for both **computer science** and **communication systems** students. Each project is for **one student** in a given semester. Students report directly to [[http://lara.epfl.ch/~kuncak|Prof. Viktor Kunčak]], even if PhD students are involved to help with various aspects of the project. The information on whether the project is available or not is also maintained only by Viktor Kunčak, so please contact him if you are interested in the project. |
| - | ===== Profile for the candidates ===== | + | ==== Nature of these projects ==== |
| - | Laboratory for Automated Reasoning and Analysis has BSc and MSc projects available (for PhD program see http://phd.epfl.ch/edic ). We are looking for students with high grades that are excellent in advanced functional programming and ideally strong in some of the core mathematical methods such as discrete mathematics, numerical analysis, logic, and probabilistic reasoning. | + | 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. Typically we expect the knowledge of courses such as [[cc|Computer Language Processing]]. |
| - | + | ||
| - | ===== Nature of these projects ===== | + | |
| - | + | ||
| - | 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. | + | |
| **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. | **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. | ||
| Line 19: | Line 13: | ||
| **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. | ||
| - | === WebAssembly Back end for Stainless === | + | ==== Example Projects ==== |
| - | + | ||
| - | Using our library to generate WebAssembly, add WebAssembly code generator to stainless, mirroring the existing JVM bytecode generator. For code generation using WebAssembly, see the later lectures at https://lara.epfl.ch/w/cc17:top . For stainless, see stainless.epfl.ch . | + | |
| - | + | ||
| - | === Robust Front End for Stainless === | + | |
| - | + | ||
| - | 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 === | === Verifying JavaScript === | ||
| Line 33: | Line 21: | ||
| Note that `(f:TObj) => e` can be encoded as `TObj(x => e)`. | Note that `(f:TObj) => e` can be encoded as `TObj(x => e)`. | ||
| - | === AST-Based Version Control === | + | === Verified Parameterized-Length Bitvectors in Stainless === |
| - | + | ||
| - | 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. | + | |
| - | + | ||
| - | === Verified Parameterized-Length Bitvectors in Leon === | + | |
| Define and prove correct a library for performing arithmetic (+, -, *, /, %) on modular arithmetic with large integers. Such operations are analogous to Int in that they perform modular arithmetic (unlike the unbounded BigInt), but the number of bits can be user-specified (unlike Int). | Define and prove correct a library for performing arithmetic (+, -, *, /, %) on modular arithmetic with large integers. Such operations are analogous to Int in that they perform modular arithmetic (unlike the unbounded BigInt), but the number of bits can be user-specified (unlike Int). | ||
| - | |||
| - | === Verifying Eliptic Curves using Leon === | ||
| - | |||
| - | Verify correctness of implementing group addition operations on elements on elliptic and Edwards curves over certain finite fields (such as those over the prime field of size 2^255-19). | ||
| - | See | ||
| - | * [[wp>Elliptic_curve]] | ||
| - | * [[wp>Edwards_curve]] | ||
| - | * [[wp>Elliptic_curve_cryptography]] | ||
| - | |||
| - | This project likely requires the previous project on parameterized-length bitvectors. | ||
| - | |||
| - | === Verify Smart Contract Code === | ||
| - | |||
| - | Verify correctness of electronic contract code. See, for example: | ||
| - | * [[wp>Ethereum]] | ||
| - | * http://www.wired.com/2014/01/ethereum/ | ||
| === Verify Security Protocol === | === Verify Security Protocol === | ||
| Propose a way to model security protocols in Leon and perform a case study to verify example protocols. | Propose a way to model security protocols in Leon and perform a case study to verify example protocols. | ||
| - | |||
| - | === Forgiving Parser for Leon === | ||
| - | |||
| - | Develop a stand-alone parser for Leon programs, which aims to accept almost any sequence of characters as input and interpret it to the best of its knowledge as a Leon program. Optionally also allow syntax supported in other programming languages. A requirement is that a valid Leon program should be interpreted in the same way as in the current front end. | ||
| - | |||
| - | More information: | ||
| - | * [[http://lara.epfl.ch/~kuncak/papers/GveroKuncak15SynthesizingJavaExpressionsFreeFormQueries.pdf|Synthesizing Java Expressions from Free-Form Queries]] | ||
| === Libraries and Applications in Stainless === | === Libraries and Applications in Stainless === | ||
| Line 78: | Line 39: | ||
| Port the **GenC** back end from Leon to stainless. This generates C code from a subset of Leon, and evaluate it on case studies for embedded code, IoT code, or fragments of OS code functinality. | Port the **GenC** back end from Leon to stainless. This generates C code from a subset of Leon, and evaluate it on case studies for embedded code, IoT code, or fragments of OS code functinality. | ||
| - | === Improve Our General-Purpose Grammar Parsing Library and grammar.epfl.ch === | + | === Parsing === |
| - | For teaching and research we are developing a library that can parse arbitrary context-free grammars, used in computer language processing course for exercises and the project, and in the future to be used in research. It is currently primarily based on generalizations of CYK algorithm as well as LL(1). Your task would be to introduce GLL, GLR, and Packrat parsing algorithms into this framework. Thanks to deep embedding, our library enables pre-analysis of grammars including the computation of first and follow sets. | + | Advance the state of the ScaLL1on parsing framework: https://github.com/epfl-lara/scallion/ |
| - | + | ||
| - | Another project in this scope is to further advance the grammar.epfl.ch web service. | + | |
| - | + | ||
| - | A version of Scala combinator library interface built on top of this library is also of interest, see e.g. (https://github.com/scala/scala-parser-combinators ). | + | |
| ===== Contact us ===== | ===== Contact us ===== | ||
| - | If one of the projects lists sounds interesting and you believe you are a suitable candide, please do not hesitate to contact Viktor Kuncak, http://lara.epfl.ch/~kuncak via email to make an appointment. In your email, please include your CV, the list of your grades, and a description of projects that you did at EPFL or outside of EPFL. | + | If one of the projects lists sounds interesting and you believe you are a suitable candidate, please do not hesitate to contact us. In your email, please include your CV, the list of your grades, and a description of projects that you did at EPFL or outside of EPFL. |
| - | + | ||
| - | Feel free to also talk to the other members of LARA group about their ongoing work and projects, see http://lara.epfl.ch | + | |