updated thesis topics

Signed-off-by: ncardozo <[email protected]>

_thesistopics/athena-elixir.md

@@ -1,6 +1,6 @@
 ---
 title: Verification and testing, together again for the first time
-period: 2024 
+period: 2025 
 level: master
 area: pil
 abstract: Create a language bridge between a formal verification language (Athena) and programming language (Elixir) to assure the correct execution of distributed systems
@@ -23,14 +23,15 @@ The effect of this conenction is that it is now posible to define proofs that ar
 ### Implementation plan
 
 The implementation of this project consists of a dual IDE in which is possible:
+
   1. Write Elixir programs that "renders" to athena verification code.
   2. Write Athena proofs that "renders" Athena code to Elixir
 
 To do this, it is necessary to create a mapping between the language abstraction of both languages, being able to run the code of each language.
 
 ### Background and Literature
 
-[1]. Fundamental Proof Methods in Computer Science: A Computer-Based Approach. MIT Press, 2017. K. Arkudas and D. Musser
+[1] Fundamental Proof Methods in Computer Science: A Computer-Based Approach. MIT Press, 2017. K. Arkudas and D. Musser
 [2] Programming Elixir. Pragmatic Bookshelf, 2018.  D. Thomas.
 
 ### Contact

_thesistopics/c-parser.md

@@ -0,0 +1,40 @@
+---
+title: A complete C grammar
+period: 2025
+level: undergrad
+area: pil
+abstract: Build a grammar and parser for the C programming language.
+people: Nicolas Cardozo
+file: c-parser
+---
+
+### Context
+
+Parsing is the first step in the analysis of programming languages. For example, to analyze the quality of software systems or to perform language transformations.
+
+To perform such analysis we are first require to encode all the grammar rules of the programming language, and then build a parser that, using our defined grammar, can recognize any program written in the language. Parsers return a tree like structure, we will be a specifc kind of tree called eCST [1] that is then use as input for our desired translation tool.
+
+Thankfully, we do not need to generate full parsers for programming languages, as this task is very complex. We can use existing parser generators, as ANTLR, that, given a grammar, can generate and efficient and correct parser for a language.
+
+In this project we want to use such a parser to translate dated C applications into a 21st century language like Rust. The first step in the translation, your project, will be to create an intermediate representation that abstract specific syntactic abstractions for an effective translation.
+
+### Project proposal
+
+The objective of this project is to take the existing grammar definition for C and compliment it with missing features in the language (deprecated or new features). The grammar must comply with the [ANTLT4][https://www.antlr.org] specification. Then, given the grammar, with the objective to generate a parser for swift.
+
+### Implementation plan
+
+1. Study the ANTLR 4 specification
+2. Review features missed by the existing C ANTLR4 grammar
+3. Extend the C grammar with missing features
+4. Generate correct eCST from concrete programas
+5. Evaluate the generated parser using different C applications with example programs from the past versions (within the last 30 years)
+
+### Background and Literature
+
+1. Rakić, N., Rakić, G., Sukur, N., & Budimac, Z. (2017, May). eCST to source code generation-An idea and perspectives. In 2017 40th International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO) (pp. 570-575). IEEE.
+2. ANTLR parser generator documentation <https://pragprog.com/titles/tpantlr2/the-definitive-antlr-4-reference/>
+
+### Contact
+
+n.cardozo

_thesistopics/linear-gleam.md

@@ -0,0 +1,43 @@
+---
+title: Linear types for Quantum computing in Gleam
+period: 2025
+level: undergrad
+area: pil
+abstract: Develop a linear type system in gleam to be used in the development of Quantum computing programs
+people: Nicolas Cardozo, Daniel Barrero
+file: linear-gleam
+layout: default
+---
+
+### Context
+
+Software verification at the type system level is used to check that programs are sound ahead of time. the idea of type systems is that if programs type-check, they will execute properly (or their strange behavior will be outside of the type system). Linear types [4], are a particular type system in which variables must be used exactly once in a program.
+
+This idea is of particular interest in the case of Quantum programming, as one of its prperties is that as soon as a q-bit is observed, it cannot longer be used.
+
+### Project proposal
+
+the objective of this project is to incorporate the ideas of linear types to a new functional programming language, Gleam [3], a BEAM-Elixir [1] compatible language.
+
+With a linear type system, it will be possible to implement Quantum programs using Gleam (based on existing Elixir libraries), that can be verified for properties as the use of q-bits, or to verify quantum cryptography protocols.
+
+### Implementation plan
+
+The implementation plan for this project is:
+
+1. Understand the theory of linear types
+2. Get familiar with Gleam
+3. Extend Gleam to incorportate linear types
+4. Build a quantum application using the linear types extension of Gleam
+
+### Background and Literature
+
+[1] Programming Elixir. Pragmatic Bookshelf, 2018.  D. Thomas.
+[2] [Quantex](https://github.com/piacerex/quantex)
+[3] [Gleam](https://gleam.run)
+[4] [Linear Types](https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=24c850390fba27fc6f3241cb34ce7bc6f3765627)
+
+### Contact
+
+n.cardozo
+dr.barrero2562

_thesistopics/parameter_verification.md

@@ -0,0 +1,47 @@
+---
+title: Verification of Parameter Passing Semantics in Actor Systems
+period: 2025
+level: undergrad
+area: pil
+abstract: Formal verification of function distribution using pass-by-move semantics in actor systems
+people: Nicolas Cardozo, Mateo Sanabria
+file: parameter_verification
+layout: default
+---
+
+### Context
+
+Programming is hard.
+
+There are two paths to help in descovering if programs actually behave as intended. First, there is validation, to state a program works under certain tested scenarios. Validation is generally the result of program testing or proof of concept applications. While validation works well, it does not provide any assurances about the program's behavior. To deal with these situations, there is verification. Verification comos from a formal mathematical proof demonstraiting without a doubt that a program satisfies a given property.
+
+Doing formal proofs for software behavior is contraintuitive. However, we can develop proofs as if we are writing programs through verification languages like Athena [1].
+
+### Project proposal
+
+In this project we are interested in a specific property of concurrent and distributed systems, function mobility. In distributed systems, the pass-by-move parameter passing semantics is defined to enable the move of parameters across nodes. This means that when a function is called with a given parameter, the parameter ceases to exist in the caller's scope, and it is moved into the callee's scope.
+
+We have explored the implementation of pass-by-move semantics as part of the implementation of cloud and distributed applications [3], based on the actor concurrency model in the Elixir language [2].
+
+With this project we want to create an Athena specification of the pass-by-move implementation to verify that, following the specification, functions move successfully, preserving their scope and sound behavior.
+
+### Implementation plan
+
+The implementation of the thesis will be developped in the Athena programming language, to verify explicitly the characteristics of Elixir actors. The implementation will require to:
+
+1. Study formal proofs and the Athena language
+2. Get familiarized with Elixir
+3. Provide an specification for Elixir actors
+4. Specify the pass-by-move semantics
+5. Verify the move behavior in Athena
+
+### Background and Literature
+
+[1] Fundamental Proof Methods in Computer Science: A Computer-Based Approach. MIT Press, 2017. K. Arkudas and D. Musser
+[2] Programming Elixir. Pragmatic Bookshelf, 2018.  D. Thomas.
+[3] [Pass-by-move elixir](https://github.com/FLAGlab/by-move)
+
+### Contact
+
+n.cardozo
+m.sanabriaa

_thesistopics/rust-parser.md

@@ -0,0 +1,40 @@
+---
+title: A complete Rust grammar
+period: 2025
+level: undergrad
+area: pil
+abstract: Build a grammar and parser for the Rust programming language.
+people: Nicolas Cardozo
+file: rust-parser
+---
+
+### Context
+
+Parsing is the first step in the analysis of programming languages. For example, to analyze the quality of software systems or to perform language transformations.
+
+To perform such analysis we are first require to encode all the grammar rules of the programming language, and then build a parser that, using our defined grammar, can recognize any program written in the language. Parsers return a tree like structure, we will be a specifc kind of tree called eCST [1] that is then use as input for our desired translation tool.
+
+Thankfully, we do not need to generate full parsers for programming languages, as this task is very complex. We can use existing parser generators, as ANTLR, that, given a grammar, can generate and efficient and correct parser for a language.
+
+In this project we want to use such a parser to translate dated C applications into a 21st century language like Rust. The first step in the translation, your project, will be to create an intermediate representation that abstract specific syntactic abstractions for an effective translation.
+
+### Project proposal
+
+The objective of this project is to take the existing grammar definition for Rust and compliment it with missing features in the language (deprecated or new features). The grammar must comply with the [ANTLT4][https://www.antlr.org] specification. Then, given the grammar, with the objective to generate a parser for swift.
+
+### Implementation plan
+
+1. Study the ANTLR 4 specification
+2. Review features missed by the existing C ANTLR4 grammar
+3. Extend the Rust grammar with missing features
+4. Generate correct eCST from concrete programas
+5. Evaluate the generated parser using different Rust programs
+
+### Background and Literature
+
+1. Rakić, N., Rakić, G., Sukur, N., & Budimac, Z. (2017, May). eCST to source code generation-An idea and perspectives. In 2017 40th International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO) (pp. 570-575). IEEE.
+2. ANTLR parser generator documentation <https://pragprog.com/titles/tpantlr2/the-definitive-antlr-4-reference/>
+
+### Contact
+
+n.cardozo

_thesistopics/uiclones.md

@@ -1,6 +1,6 @@
 ---
 title: Clone detection for UI elements
-period: 2024
+period: 2025
 level: undergrad
 area: pil
 abstract: Detection of code clones across interface elements for Kotlin and Dart codebases
@@ -34,7 +34,7 @@ The implementation plan of this thesis is focused on the extension of the Out Of
 ### Background and Literature
 
 - [1] Clone detection
-- [2] OOS
+- [2] Out Of Step:  https://www.sciencedirect.com/science/article/pii/S0167642324000352
 
 ### Contact