PhD Position F/M Resource-Aware Conservative Static Analysis
Contract type : Fixed-term contract
Level of qualifications required : Graduate degree or equivalent
Fonction : PhD Position
About the research centre or Inria department
The Inria University of Lille centre, created in 2008, employs 360 people including 305 scientists in 15 research teams. Recognised for its strong involvement in the socio-economic development of the Hauts-De-France region, the Inria University of Lille centre pursues a close relationship with large companies and SMEs. By promoting synergies between researchers and industrialists, Inria participates in the transfer of skills and expertise in digital technologies and provides access to the best European and international research for the benefit of innovation and companies, particularly in the region.For more than 10 years, the Inria University of Lille centre has been located at the heart of Lille's university and scientific ecosystem, as well as at the heart of Frenchtech, with a technology showroom based on Avenue de Bretagne in Lille, on the EuraTechnologies site of economic excellence dedicated to information and communication technologies (ICT).
Context
The PhD student will be part of the SyCoMoRES team of Inria Lille & CRIStAL lab, which currently hosts 4 fellow PhD students and one postdoc. Lille is a city close to Brussels, Paris & London, easily reachable by train, with a large student population and a number of cultural places & events. The lab has a very active equality and parity commission, which raises awareness on this topic to all staff (with specific events for newcomers), and provides outreach activities for high-schoolers. One of the advisors (Raphaël Monat) is an active member of this commission.
PhD students are appointed for a duration of 3 years. We plan to organize weekly research meetings with the PhD student. In addition, the student will be able to attend monthly meetings with other Mopsa practitioners. This research project is part of ANR JCJC RAISIN. We will hold quarterly project meetings with Sophie Cerf (member of the project), who is a researcher at Inria with expertise in control theory for software systems
Assignment
**Start date flexible. Informal enquiries are welcome by email, reach out to Raphaël Monat**
One approach aiming at reducing the number of bugs is static program analysis through the framework of abstract interpretation [1]. Contrary to dynamic analyses such as fuzzing [7], the program is not executed but its source code is analyzed. Thanks to this approach, the analysis conservatively considers all possible execution paths of the program during the analysis, ensuring the absence of false negatives. In addition, the analyses are automatic: they do not require any user interaction to complete their task and they will be completed in a guaranteed finite time. These analyses can be seen as “push-button” as no expert knowledge is required to run them. This approach has been particularly successful to certify the absence of runtime errors in critical embedded C software. Astrée [2] has proved the absence of runtime errors in software of Airbus planes.
The daily use of conservative static analyzers by non-experts remains a challenge. First, these tools offer a wide range of configuration options which is difficult to choose from. Each option will have a different impact on the performance-precision tradeoff of the analysis, that will also vary depending on the considered program. Mansur et al. [5], Heo et al. [3] have looked into ways to automatically choose options to attain the highest precision when analyzing a program, given a resource envelope (CPU time, memory usage); but their approaches are however limited in terms of scalability. Second, most static analyzers cannot express their progress during an analysis, which results in an unfriendly black-box behavior. The overall goal of this thesis is to address these two usability barriers. We plan to explore the following research directions:
• Estimating the experimental complexity of analyzing a given program. In the static program analyses we consider, we hypothesize that the complexity of analyzing a program is mostly impacted by the number of programs loops and function calls, the maximum depth of these nested constructs. We will need to confirm this hypothesis, and then focus on finding measures of the complexity of a
program’s analysis. We will start by considering a simplified setting focusing on a toy imperative language. In a way, this complexity measure will be an analysis of the program analysis itself. If needed, we will consider additional, yet realistic, hypotheses on the convergence of widening used during loop analysis.
• Estimation of remaining analysis time. This estimation will be performed online (i.e, during the analysis), when the full configuration of the static analyzer is fixed. Current static analyzers are often guaranteed to terminate in finite time, but do not provide any estimate of the remaining analysis time. We plan to go beyond the work of Lee et al. [4] by developing a semantic, language-independent and domain-independent progress bar that will work with fully relational numerical abstract domains.
• Offline choice of best configuration. We plan to develop techniques finding the configurations yielding the most precise analyses of a given program. We will start by investigating a posteriori techniques where the analyzer suggests precision improvements to remove some of the alarms it found (e.g, by suggesting to enable specific options). We will then consider a priori techniques relying on pre-analyses to find the best configuration options to analyze a program. Combined with an estimation of the cost of analyzing the program in a given configuration, we will be able to find a configuration reaching the best precision while respecting a pre-specified resource envelope. We will leverage the partial order on the precision of analyzers to guide our exploration.
Main activities
The candidate will work in the overall field of formal methods and programming language theory. They will work on conservative static analyses, and in particular some rooted in the framework of abstract interpretation. We expect the successful candidate to be motivated to improve experimental research tools such as Mopsa, which is implemented in the OCaml functional programming language.
Benefits package
- Subsidized meals
- Partial reimbursement of public transport costs
- Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
- Possibility of teleworking and flexible organization of working hours
- Professional equipment available (videoconferencing, loan of computer equipment, etc.)
- Social, cultural and sports events and activities
- Access to vocational training
- Social security coverage
General Information
- Theme/Domain : Proofs and Verification
- Town/city : Villeneuve d'Ascq
- Inria Center : Centre Inria de l'Université de Lille
- Starting date : 2025-09-01
- Duration of contract : 3 years
- Deadline to apply : 2025-04-14
Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.
Instruction to apply
Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.
Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.
Contacts
- Inria Team : SYCOMORES
-
PhD Supervisor :
Monat Raphael / raphael.monat@inria.fr
About Inria
Inria is the French national research institute dedicated to digital science and technology. It employs 2,600 people. Its 200 agile project teams, generally run jointly with academic partners, include more than 3,500 scientists and engineers working to meet the challenges of digital technology, often at the interface with other disciplines. The Institute also employs numerous talents in over forty different professions. 900 research support staff contribute to the preparation and development of scientific and entrepreneurial projects that have a worldwide impact.