The goal of this PhD is to further the potential of model-based formal verification of black-box systems by combining model-learning techniques with formal methods. This tight integration of formal methods into the learning process will help in producing high-quality models automatically, and steering the learning process towards areas that are of interest and/or lacking precision during the learning process. Your responsibilities will include:  

• Research and development of novel model-learning approaches and their integration into the model-learning library AALpy (GitHub - DES-Lab/AALpy). 
• Investigating the step from a learned model towards formal verification techniques such as invariant detection, model-checking, monitoring and shielding.
• Systems under verification include machine-learned systems, LLM-generated code, autonomous agents, embedded systems.
• Development and demonstration of a black-box verification workflow for one or two selected verification techniques in combination with model learning. 
• Scientific collaboration with renowned universities and research organizations. 
• Scientific publications in high-impact journals and presentations at major conferences. 
• Possible specialization topics include LLMs, real-time, non-functional properties and verification of machine-learned agents.

 
As a PhD student in the CRYSTALLINE program, you will become a member of the SAL Doctoral College (SAL-DC) that actively fosters networking and collaboration among students and supervisors, as well as the discussion and exchange of ideas in a diverse interdisciplinary setting. For supporting our interdisciplinary environment, there will be dedicated events and platforms including our annual summit, our scientific forum, summer schools, social activity days, etc. This specific PhD position will be organized in cooperation with Graz University of Technology, Bernhard Aichernig serving as the main supervisor from TU Graz. The doctoral degree will be awarded within the doctoral school of computer science at TU Graz. Co-supervision will be performed Martin Leucker from Lübeck University.

• Application deadline: 3 November 2024
• Weekly working hours: 38.5
• Diversified research activities with plenty of technical challenges.
• State-of-the-art lab facilities and instruments.
• Internal and external training opportunities for further development.
• Home Office possible.
• € 4 per day food allowance in restaurants or € 2 per day in supermarkets.
• Family & kids friendly.
• Free coffee/milk/tea & fresh fruits.

For this position you will receive a monthly gross salary of EUR 3,827, which will be paid 14 times a year. Financial support for housing for stays abroad (e.g., in case of secondments) and travelling expenses will be offered on a case-by-case basis.

Silicon Austria Labs (SAL) is a top research center for Electronics and Software Based Systems (ESBS). At three locations (Graz, Villach, Linz), SAL is conducting research along the entire ESBS value chain in the areas of sensor systems, power electronics, intelligent wireless systems, microsystems and embedded systems to develop future-oriented solutions for industrial production, health, energy, mobility, safety and more. SAL brings together key players from industry, science and research and thus valuable expertise and know-how and conducts cooperative, application-oriented research along the value chain. Cooperative projects are co-financed by SAL and enable a fast and unbureaucratic project start. SAL is thus shaping the high-tech location Austria and Europe and developing the future