Thesis and Internships

Below you can find the thesis topics offered by SELAB and SSE to bachelor and master students. If you are interested in one of the topics, please contact the (co-)supervisor (add the identifier of the thesis topic in your email)

  • [T30] A regression test suite for Eiffel Base
  • Suitability: Master's thesis or Research in computer science
  • Description: One of the advantages of programming in a language supporting Design by Contract is that contracts make for automatic testing oracles, based on which we can automatically generate test cases using frameworks such as AutoTest. In practice, however, the tests generated automatically are only as good as the available contracts. Therefore, it would still be useful to have accurate manually written test cases, to be used for regression testing and as an independent benchmark to measure the effectiveness of other techniques based on tests. The goal of this project is to build a comprehensive regression test suite for the data structure classes in EiffelBase and Gobo, the two major Eiffel standard libraries. The tests should be accurate and as complementary as possible to those that AutoTest normally produces with the available contracts.
  • [T31] EVE-Pink: Discovering loop invariants by postcondition weakening
  • Suitability: Master or Bachelor's thesis
  • Description: Loop invariants are an indispensable ingredient to perform correctness proofs of programs. At the same time, annotating a loop with significant invariants is often difficult and tricky. The availability of postconditions can help in this regard, as loop invariants can often be expressed as a weakening of post-conditions. In this project, you will be asked to implement a loop invariant inference technique based on postcondition weakening. The implementation will re-design and improve the current prototype, and integrate it within a development environment.
  • [T32] FOL4All: Complex loop invariants with a theorem prover
  • Suitability: Master's thesis or Research in computer science
  • Loop invariants are necessary to verify any non-trivial program. At the same time, they are more difficult for a programmer to write than other annotations (such as pre and postconditions). This suggests that techniques to automate the inference of loop invariants can have a very significant impact and improve software verification in practice. This project considers an approach [KV09] to find loop invariants based on translating the semantics of loops into first-order formulas. These formulas are then analysed with a fully-automated saturation theorem prover (such as Vampire). The theorem prover generates all consequences of the loop's semantics, among which are loop invariants. The approach is best-effort, because the generation of the possible invariants cannot be exhaustive, but it can be effective in practice and generate complex invariants for some loops. In this project, you will develop and implement a loop analysis engine based on translation of loops in first-order formulas to be manipulated by a saturation theorem prover. The translation leverages intermediate languages that provide various abstraction levels, from the program source down to first-order logic.
  • [T33] LAAID (Loop Analysis And IDentikit): An empirical analysis of loops
  • Suitability: Bachelor thesis
  • Loops are the hardest part when it comes to reasoning about a program. Several techniques for automating reasoning about loops have been developed, each placing a particular restriction on the loops it can handle (e.g., the number of nested loops, the type of operations in the loop body, etc.). It is not known, however, how does the "usual" loop look like, how complex it is, and how far is the state-of-the-art from being able to handle these most frequently occurring loops automatically. In this project, you will develop a few metrics to characterise the complexity of loops with respect to the currently available technology for automated proofs, and you will mine codebases in various languages to determine what kind of loops are most commonly found in programs.
  • [T34] Eve plug-in for detection of inconsistent contracts
  • Supervisor: Victor Rivera
  • Co-Supervisor: Alexander Naumchev
  • Suitability: Bachelor's thesis
  • The task is to study an existing methodology for detection of inconsistent contracts and implement it as a part of Eiffel Verification Environment.
  • [T35] Eve plug-in for detection of weak contracts
  • Supervisor: Victor Rivera
  • Co-Supervisor: Alexander Naumchev
  • Suitability: Bachelor's thesis
  • The task is to study an existing methodology for the detection of weak contracts and to implement it as a part of Eiffel Verification Environment.
  • [T36] A Byte-Code Analyzer for Android Apps
  • Supervisor: Néstor Cataño
  • Suitability: Bachelor's thesis
  • See description here
  • [T37] Où Sortir? (Where to go?)
  • Supervisor: Néstor Cataño
  • Suitability: Bachelor's thesis
  • See description here
  • [T38] A Facebook Plugin for Privacy-Aware Social Networking
  • Supervisor: Néstor Cataño
  • Suitability: Bachelor's thesis
  • See description here
  • [T39] Development of a JML Library in Yices
  • Supervisor: Néstor Cataño
  • Suitability: Bachelor's thesis
  • See description here
  • [T40] Implementation of a Constraint Solver for EventB2Java
  • Supervisor: Néstor Cataño
  • Suitability: Bachelor's thesis
  • See description here
  • [T41] Open-source Projects
  • Supervisor: Victor Rivera
  • Co-Supervisor: Alexander Naumchev
  • Suitability: Bachelor's thesis
    1. You (students) choose an active open-source project to work on.
    2. You propose new functionality that you want to add to the project.
    3. We agree on your proposal (this need to be done before the start of the thesis work).
    4. You develop the proposed functionality; I serve as a mentor that tracks your progress and helps in overcoming impediments.
    5. (Optional) We attempt to integrate your development to the open-source project; acceptance of the code by the community will immediately make your contribution visible to the World.

Below you can find the thesis topics currently in progress by SELAB and SSE students

  • [T2] Simulation of cloud computation
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Leonard Johard
  • Student: Chernyshov Alexey
  • [T3] BioDynaMo: Cloud simulation implementation
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Leonard Johard
  • Student: Kosterin Alexey
  • [T4] VR/Advanced visualization for neuroscience simulation
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Leonard Johard
  • Student: Trusov Alexey
  • [T5] Reinforcement learning: Value function approximation for autonomous control
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Leonard Johard
  • Student: Mazaeva Ekaterina
  • [T6] BioDynaMo: Spatial organization
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Leonard Johard
  • Student: Drobnyy Vicktor
  • [T7] Pseudorehearsal in actor-critic learning algorithms
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Leonard Johard
  • Student: Marochko Vladimir
  • [T8] Reinforcement learning in robotics
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Leonard Johard
  • Student: Nikolaev Evgenii
  • [T9] BioDynaMo: Optimization of Physics Engines
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Leonard Johard
  • Student: Dmitrenok Ilya
  • [T10] Data compression and Neural Networks
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Leonard Johard
  • Student: Koreneva Mariya
  • [T11] Data compression and Genetic Algorithms
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Leonard Johard
  • Student: Tkachuk Vladislav
  • [T12] Developing a searching mobile application
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Leonard Johard
  • Student: Davletshina Diana
  • [T13] Developing distributed server control panel
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Larisa Safina
  • Student: Zhdanov Anton
  • [T28] Security in Microservices Architecture
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Larisa Safina
  • Student: Minakova Olga
  • [T14] Semantic mapping of natural language into abstract Hoare triples (and back)
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Alexander Naumchev
  • Student: Skukov Vladislav
  • [T15] Semantic mapping of natural language into abstract Hoare triples (and back)
  • Supervisor: Victor Rivera
  • Co-Supervisor: Alexander Naumchev
  • Suitability: Bormotova Anastasia
  • [T16] A theoretical Framework for Static Type Checking of Clojure
  • Supervisor: Manuel Mazzara
  • Student: Tropin Andrew
  • [T17] Developing complete library of SMT statements to support Jolie type-checking
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Larisa Safina, Daniel de Carvalho
  • Student: Mingela Bogdan
  • [T18] Verified type checker for Jolie programming language
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Larisa Safina, Daniel de Carvalho
  • Student: Akent'ev Evgeny
  • [T19] Video Search and Microservices
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Larisa Safina
  • Student: Kasatkin Timur
  • [T20] Static type checking for Jolie programming language
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Larisa Safina
  • Student: Troshkov Nikolay
  • [T21] Running Django applications on AWS Lambda
  • Supervisor: Victor Rivera
  • Co-Supervisor: Larisa Safina
  • Student: Kurilenko Nikita
  • [T22] Anonymisation of SN using Constraint Programming
  • Supervisor: Victor Rivera
  • Student: Solonets Sergey
  • [T23] Inferring locations that can change its value
  • Supervisor: Victor Rivera
  • Student: Bandura Alexey
  • [T24] Optimization of information systems for automatization of business-processes in sense of performance and scalability in conditions of industrial projects
  • Supervisor: Victor Rivera
  • Student: Fomchenko Nikita
  • [T25] Development of user interfaces for working with different datasets in conditions of industrial project
  • Supervisor: Victor Rivera
  • Student: Kamsky Athur
  • [T26] Developement of information systems for automatization of business-processes in conditions of industrial projects
  • Supervisor: Victor Rivera
  • Student: Skoriukov Maksim
  • [T27] Eiffel code generation for Event-B models
  • Supervisor: Victor Rivera
  • Student: Krikun Giorgiy
  • [T29] Microservice architecture development for computing system with 15-years (and more) life-cycle
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Larisa Safina
  • Student: Plyusnin Ivan

Below you can find the thesis already finished

Below you can find the thesis topics offered by SELAB and SSE to bachelor and master students

  • [Alias-analysis1] Help develop a way to find out if two pointer/reference expressions can ever point to the same object at run-time
  • Supervisor: Bertrand Meyer, Victor Rivera
  • Student: 3
  • [Frame-analysis1] Help develop a way to find out if an operation can change the value of an expression
  • Supervisor: Bertrand Meyer, Victor Rivera
  • Student: 3
  • [Eiffel-inspector1] Devise (invent!) new properties to check for quality Eiffel programs, and add these checks to the Eiffel Inspector static analyzer
  • Supervisor: Bertrand Meyer, Victor Rivera
  • Student: 3
  • [Jolie1] Construction of static type checking for a dynamically typed language
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Larisa Safina
  • Student: 5
  • [Intelligent-buildings1] Data collection and analysis, behavioural patterns identification. Construction of AI room manager.
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Larisa Safina
  • Student: 3
  • [Microservices1] Work on case studies and literature review.
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Larisa Safina
  • Student: 2
  • [BioDynaMo1] Multiple tasks related to the project: https://biodynamo.web.cern.ch/ (visualization, data structures, simulation)
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Leonard Johard
  • Student: 6
  • [Reinforcement-learning1] Implementing algorithms for reinforcement learning neural networks in games and simulators
  • Supervisor: Manuel Mazzara
  • Co-Supervisor: Leonard Johard
  • Student: 2
  • Several Topics on Eiffel Studio Technology
  • Supervisor: Bertrand Meyer, Victor Rivera
    1. Extension of Time library with time zones, daylight savings, calendars and associated conversions.
    2. Extension of Time library with new input-output formats: partial date and time, time zones.
    3. Extension of Time library with built-in support for ISO-8601 and several RFC date/time formats, including Unicode support and factory-based extendible API for arbitrary input-output date/time formats.
    4. A composer for ITERABLEs.
    5. A task library for SCOOP. Tasks get executed by a processor pool, their results can be reported synchronously or asynchronously.
    6. Conversion of eweasel (and/or some other tool) to SCOOP.
    7. Static prevention of deadlocks in SCOOP programs. The idea is to introduce a set of compile-time rules that guarantee absence of wait cycles.
  • [AutomaticRepair] Automatic program repair: making the analysis faster.
  • Supervisor: Bertrand Meyer, Victor Rivera
  • Student: 1
  • [Alias-analysis2] Applying alias analysis to deadlock analysis in concurrent computation.
  • Supervisor: Bertrand Meyer, Victor Rivera
  • Student: 1
  • [Autoproof1] Adapting the AutoProof program verification system to void safety.
  • Supervisor: Bertrand Meyer, Victor Rivera
  • Student: 1
  • [Autoproof2] Fully verified Algorithms
  • Supervisor: Bertrand Meyer, Victor Rivera
  • Student: 1
  • Development of new examples of fully algorithms with correctness proofs in the AutoProof program verification system.
Сайт находится в технической разработке