Differences

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

--- projects [2017/04/11 11:43]
vkuncak
+++ projects [2018/08/22 14:45]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Available Student Projects in LARA - EPFL Internal Page ======
-**(c) 2016 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 Kuncak.**
 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.
@@ Line 19: / Line 19: @@
 **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 Generation Library for Scala ===
+=== WebAssembly Back end for Stainless ===
-Write a library for generating WebAssembly code, to be used in Computer Language Processing course as well as for other projects in the community. This library might replace the Cafebabe library: https://github.com/psuter/cafebabe
+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 Leon Compiled Using scala.js ===
+=== 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.
@@ Line 36: / Line 36: @@
 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 ===
-Do you know Wandida videos? These famous videos explain concepts using natural drawing, pictures, voice. Although very popular, it is hard to produce them. Their greatest limitation is that they are hard to modify and long to produce, with a lot of post-processing.
-To simplify this process, we will adopt a vectorized format more suitable to integration with other presentation elements (inline quizz, textual slides, text-to-speech, embedding, hypertext linking, etc.)
-The student will have define this format, create sample explanation videos, and possibly adapt leon.epfl.ch to let users produce such videos very quickly.
-As a long-term result this project will enable the creation of much more such videos which are very appreciated by students.
-=== Reversing Embedded Domain Specific Languages (DSL) ===
-To make programming easier, people use languages adapted to a particular domain, in order to write less. For example, when creating web pages from Scala code, one can start to define DSL so that instead of writing `Element("div", List(TextElement("hello "+"world")))`, one can simplify write `<.div("hello "+"world")`.
-We recently wrote an engine which, given a modification of text *on the web page* (ex: hello to bonjour), is able to modify the string from the original expression, whatever the way it was built <.div("bonjour "+"world"), even asking questions in the case of ambiguities.
-The student would push this feature towards having full HTML tree edition, but at the same time reconstructing the smallest DSL expression that can support the change in the output.
-As an immediate result one will be able to create and modify presentation using reveal.js.
-=== Database filling in Programming by Example ===
-We recently designed a model for modifying program-generated webpages so that it modifies the original program, yielding a very useful programming environnement where both the program and the output can be modified.
-However, we would like to extract data from the program (e.g; text, svg data, animations, audio...) so that the parsing becomes faster and the data is stored in a structured way.
-For that, the student will have to come up with creative ways to 1) Store such data in the server 2) Retrieve it from a program 3) Modify this data when the output changes 4) Modify the *structure* of the data if the program change.
-As an immediate result one will be able to record audio in html slides, or add SVG animations.
 === Verified Parameterized-Length Bitvectors in Leon ===
@@ Line 89: / Line 68: @@
   * [[http://lara.epfl.ch/~kuncak/papers/GveroKuncak15SynthesizingJavaExpressionsFreeFormQueries.pdf|Synthesizing Java Expressions from Free-Form Queries]]
-=== Libraries and Applications in Leon ===
+=== Libraries and Applications in Stainless ===
-Develop and specify additional applications and/or libraries for Leon 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.
+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.
-=== Improve Leon Web-Based IDE ===
+=== C Back-End for a Stainless Subset ===
-Develop new IDE functionality and interactive program transformations for Leon. The transformations should subsume refactorings present in e.g. Eclipse IDE, but should also make use of Leon's ability to check correctness conditions to ensure soundness of transformations.
-=== Statistically Biased Code Generation ===
-Develop statistical models for a class of useful Leon programs and use them to build code completion functionality as well as to improve deductive synthesis of Leon.
-For more information, please check the notion of a Java language model from the report [[http://infoscience.epfl.ch/record/201606/files/main.pdf|On Synthesizing Code from Free-Form Queries]], and also consult the notion of statistical language model from natural language translation literature (e.g. http://www.cs.colorado.edu/~martin/slp.html ).
-=== C Back-End for a Leon Subset ===
-Advance our **GenC** back for Leon, which 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 ===