CRYSTALLINE PhD position - Model Learning and Formal Methods (all genders) // Job-ID: 146-1

Your future responsibilities

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.

Your profile

• MSc in Computer Science or a related field with a strong academic record.
• Background and interest in formal methods is beneficial.
• Strong coding and algorithmic skills (mainly Python for AALpy and pytorch).
• Special interest in model learning, automata theory, real-time systems, machine learning, LLMs… is beneficial.
• Excellent written and oral communication skills in English.
• Enthusiasm for developing new ideas and a positive attitude towards new challenges. 
• Ability to work independently, be well organised, produce high quality documents and meet deadlines. 
• Project experience and/or publications in related fields are beneficial.

Important Facts about SAL

• 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 after alignment with the supervisor and the CRYSTALLINE program leader.

Become part of Silicon Austria Labs

Application requirements:

• Applicants must not have resided and/or carried out their main activity (work, studies, etc.) in Austria for more than 12 months in the 3 years immediately before the call deadline.
• Master's degree including official evidence completed by application deadline.
• Not in possession of a PhD degree.
• Only complete sets of application documents concatenated in a single PDF can be accepted.

Required application documents (concatenated in a single PDF in this order):

• [Mandatory] 1-page letter of motivation (in English), including a declaration of the considered research topic
• [Mandatory] CV (in English), including
  • expertise, skills, and
  • (if applicable) list of internships and publications & patents
• [Mandatory] Scanned copies of transcripts of records for bachelor and the master (or equivalent degree) including the diplomas proofing the completion of the studies (originally issued in English or German, or an official translation in alignment with the guidelines on translation and authentication)
• [Mandatory] Proof of fluency in English at minimum B2 level (Upper Intermediate English). Accepted proofs are e.g. master studies in English or an internationally accepted certificate.
• [Mandatory] Scanned copy of valid Passport/ID
• [Optional] Letter of references from academic reference persons (with contact details)
• [Optional] Authored/Co-authored publications
• [Mandatory] Master thesis

Please check all the details about the application requirements on our website: Crystalline Program Recruitment | SAL Research Network (silicon-austria.com)