The objective of this position is to develop a method that will allow finding software problems in GPU software as well as proving the correctness of the GPU software and that it adheres to its specification through the use of formal methods.
The work involves experimenting with an existing formal technology for CPUs and extend it for use in a GPU environment. Moreover, it includes the evaluation of the capabilities of these methods, such as what types of errors are possible or impossible to be find with them. For the experimental assessment space relevant software will be ported to the formal method framework selected for the project. The work will be performed within the context of the Formal Methods for GPUs project funded by the European Space Agency (ESA), which is coordinated by BSC.
The student is expected to enroll or have already been enrolled in a Bachelor’s program. The technical work performed during the candidate’s placement will contribute to the student’s Bachelor’s Thesis. Upon successful completion of the Bachelor’s degree, the student may be offered the possibility to continue for a Master’s degree, leading to PhD studies.
Key Duties
Evaluate existing formal methods frameworks for CPUs for safety-critical systems use
Evaluate experimental formal methods frameworks for GPUs for safety-critical systems use
Adapt space relevant software for the demonstration of the capabilities of these methods
Develop additional methods which can enhance the capabilities for these methods or make them more appropriate for GPUs
Termini per aplicar: Divendres, 30 Juny, 2023
Més entrades de Beques
Comentaris