Differences

This shows you the differences between two versions of the page.

--- projects [2019/12/16 15:47]
vkuncak
+++ projects [2021/10/27 11:25]
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 Kunčak.**
+General LARA Projects Suggestions: https://gitlab.epfl.ch/kuncak/student-projects/
-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.
+In Spring 2022 we will accept only a limited number of semester projects of students who took Computer Language Processing or Formal Verification, because Viktor Kuncak is on a sabbatical.
-==== 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. Typically we expect the knowledge of courses such as [[cc|Computer Language Processing]].
-**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.
-==== Example Projects ====
-=== 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)`.
-=== Verified Parameterized-Length Bitvectors in Stainless ===
-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).
-=== Verify Security Protocol ===
-Propose a way to model security protocols in Leon and perform a case study to verify example protocols.
-=== Libraries and Applications in Stainless ===
-Develop and specify additional applications and/or libraries for Stainless system, along with their specifications. Examples of applications include parsing algorithms, compilers, email clients, web applications (e.g. a news portal). Examples of libraries include data structures, linear algebra libraries, user interface libraries, as well as sound and graphics processing libraries.
-Among possible directions is to use http://www.scala-js.org/ to generate Javascript from Leon. To make such code useful, explore building Leon libraries that interface to Javascript APIs (focusing to the extent possible on stateless APIs) and build Leon specifications and stubs that approximate the behavior of these APIs to enable verification and synthesis.
-=== C Back-End for a Stainless Subset ===
-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.
-=== Parsing ===
-Advance the state of the ScaLL1on parsing framework: https://github.com/epfl-lara/scallion/
-===== Contact us =====
-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.