Symbolic execution of Fortran programmes
Supervisor: Nikolaus Huber
Project description
As one of the oldest programming languages still in active use, Fortran remains a key platform for high-performance computing, particularly in science, engineering and finance. CamFort is a programme analysis and verification tool developed at the University of Cambridge that helps developers improve the correctness, maintainability and reliability of Fortran code.
The aim of this internship is to extend CamFort with symbolic execution capabilities. Symbolic execution is a powerful programme analysis technique that systematically explores programme paths using symbolic inputs, enabling the detection of subtle and deep-seated bugs in complex codebases.
Depending on the student’s interests, the project may explore several directions, including applying symbolic execution to different verification tasks, integrating it with existing CamFort analyses, or investigating synergies between symbolic execution and other static analysis methods supported by the tool.
Working environment
The student will have weekly meetings with the supervisor to assess the progress and discuss blocking issues. There is a possibility for the student to join regular group meetings within ICCS if they are interested, and to attend the ICCS Summer School. While the student is expected to be available for meetings in person, some remote work can be discussed and accommodated.
Essential knowledge, skills and attributes
- Basic functional programming skills (preferably in Haskell)
- Knowledge of compiler construction (eg. parsing, abstract syntax trees, intermediate representations)
- Experience with programme verification is an advantage, but not essential.
Contact us
If you have questions about this project, email Nikolaus Huber.