Tuesday, 3 June 2025

Two Open PhD Positions as Graduate Teaching Assistant

I'm building up my new research group on Formal Methods at Johannes Kepler University Linz (JKU), Austria, and currently have two open PhD positions as Graduate Teaching Assistants:

🔗 Job Posting Link

If you're interested in Specification, Verification, Falsification, and Automata Learning (yes – we learn formal models!), and want to pursue a PhD, please apply!

My Institute for Formal Models and Verification (FMV) is responsible for courses such as Formal ModelsModel CheckingDebugging, and other research-aligned special topics.

I'm also a Key Researcher in the BilAI Cluster of Excellence, which focuses on integrating symbolic and sub-symbolic AI.

I work closely with my PhD students, including weekly one-to-one meetings.

Deadline: July 2, 2025

📨 Looking forward to your application!

Thursday, 10 April 2025

CV

Bernhard K. Aichernig is a full professor of Formal Methods at Johannes Kepler University Linz (JKU), Austria, where he leads the Institute of Formal Models and Verification (FMV). His research focuses on the foundations of software engineering for dependable and trustworthy systems, with interests in automated falsification, verification, and modelling. Current topics include automata learning, learning-based testing, and the integration of symbolic and subsymbolic AI. He is the author of more than 140 scientific publications. 
Until April 2025, he was affiliated with Graz University of Technology. From 2002 to 2006, he held a faculty position at the United Nations University in Macao, China. He served on the board of Formal Methods Europe from 2004 to 2016. Prof. Aichernig holds a habilitation in Practical Computer Science and Formal Methods, a doctorate, and a Diplom-Ingenieur degree, all from Graz University of Technology.

Tuesday, 1 April 2025

New Position at JKU

I started on April 1st as Professor of Formal Methods at Johannes Kepler University in Linz, where I’m now heading the Institute of Formal Models and Verification.

This marks a new chapter after more than 27 years at Graz University of Technology, interrupted only by four years at UNU in Macau (2002–2006). It was a fantastic time at TU Graz, and I’m very grateful to my alma mater for all the opportunities, collaborations, and support over the years.

I’m looking forward to working with my new colleagues at JKU and continuing research and teaching in formal methods. Let’s make systems not only more intelligent — but also more dependable and trustworthy.

Tuesday, 23 January 2024

Activities in 2024

 

  • Dean of Studies of the Faculty of Computer Science at TU Graz
  • Key Researcher in three research projects: LearnTwinsAIDoARt (both projects got extended), and TASTE.
  • Co-Manager and key researcher of the  TU Graz - SAL Dependable Embedded Systems Lab (DES Lab) 
  • Steering board member of TAP, the International Conference on Tests and Proofs
  • Co-Organizer of the track on AI-Assisted Programming at AISOLA 2024.
  • Invited speaker at the following events:
    • LearnAut 2024, 5th workshop on Learning and Automata, 7 July 2024, Tallinn, Estonia.
    • AISOLA 2024, 2nd Artificial Intelligence ISoLA, Track on AI-Assisted Programming, 30 Oct - 3 Nov 2024, Crete, Greece.
  • 10 peer-reviewed publications:
    • 4 journal articles
    • 6 conference articles, including three A*-conferences (ICSE and ACL)
  • PC Member of several peer-reviewed conferences and workshops, including
    • ECAI 2024, 27th European Conference on Artificial Intelligence
    • FMICS 2024, 29th International Conference on Formal Methods for Industrial Critical Systems
    • A-MOST 2024, 20th Workshop on Advances in Model Based Testing
  • Teaching 
    • Software Paradigms (Bachelor-level)
    • Declarative Programming (Bachelor-level)
    • Quality Assurance in Software Development (Bachelor-level)
    • Model-based Testing (MSc-level)
  • PhD supervision of
    • Edi Muskardin (defended on September 17th with distinction)
    • Felix Wallner
    • Benjamin von Berg
  • External PhD reviewer and opponent of Wenjing Chu, Leiden University, the Netherlands (defended on December 4th).

Tuesday, 14 November 2023

Activities in 2023

 

Tuesday, 13 December 2022

Activities in 2022

 Here is a summary of my activities in 2022.

  • Key Researcher in three research projects Dependable ThingsLearnTwins, and AIDoARt
  • Co-Head and key researcher of the  TU Graz - SAL Dependable Embedded Systems Lab (DES Lab) 
  • Steering board member of TAP, the International Conference on Tests and Proofs
    • PC Member of 
      • FORMATS 2022,  the 20th Intern. Conference on Formal Modeling and Analysis of Timed Systems
      • SAC 2022, 37th ACM/SIGAPP Symposium on Applied Computing
      • A-MOST 2022, 18th Workshop on Advances in Model Based Testing
    • Member of the selection board for external master students in the programme Software Engineering and Management
    • Teaching 
      • Software Paradigms (Bachelor-level, 287 students)
      • Declarative Programming (Bachelor-level, 266 students)
      • Quality Assurance in Software Development (Bachelor-level, 204 students)
      • Model-based Testing (MSc-level)
      • Formal Specification and Design of Software (MSc-level)

    Friday, 29 October 2021

    Activities in 2021

     Here is a summary of my activities in 2021. This list will be updated as tasks come along.

    • Key Researcher in three research projects Dependable Things, LearnTwins, and AIDoARt
    • Co-Head and key researcher of the  TU Graz - SAL Dependable Embedded Systems Lab (DES Lab) 
    • Invited speaker at the AVL ITS R&T Research Networking Day 2021 and ISOLA 2021
    • Steering board member of TAP, the International Conference on Tests and Proofs
      • PC Member of 
        • FM 2021, 24th International Symposium on Formal Methods
        • ICTAC 2021, 18th International Colloquium on Theoretical Aspects of Computing
        • TAP 2021, 15th International Conference on Tests and Proofs
        • IFIP ICTSS 2021, 33rd International Conference on Testing Software and Systems
        • A-MOST 2021, 17th Workshop on Advances in Model Based Testing
        • ITEQS 2021, 5th International Workshop on Testing Extra-Functional Properties and Quality Characteristics of Software Systems
        • SAC 2022, 37th ACM/SIGAPP Symposium on Applied Computing
      • Reviewer for the journals
      • External examiner at the PhD defence of Niveditha Manjunath, TU Vienna: Fault-Based Analysis of Cyber Physical Systems.
      • Member of the selection boards for external master students in the programmes Computer Science and Software Engineering and Management
      • Teaching 
        • Software Paradigms (Bachelor-level, 207 students)
        • Declarative Programming (Bachelor-level, 190 students)
        • Quality Assurance in Software Development (Bachelor-level, 165 students)
        • Model-based Testing (MSc-level)
        • Formal Specification and Design of Software (MSc-level)

      Thursday, 3 September 2020

      Postdoc position on Formal Methods and Testing @ TU Graz, Austria

      I am looking for a University Assistant (postdoc) to join my research group at Graz University of Technology, Austria. We do research in the areas of formal methods, testing and automata learning.  The group combines verification, falsification, modelling, and learning.

      The postdoc will do fundamental research in the new TU Graz-SAL Dependable Embedded Systems Lab (DES Lab) where we research new methods for zero-bug software and dependable AI. In the DES Lab she/he will collaborate with SAL (https://silicon-austria-labs.com) and a team around six well-known researchers of TU Graz: Marcel Baunach (embedded systems), Roderick Bloem (verification, synthesis), Robert Legenstein (computational neuroscience, machine learning), Stefan Mangard (security), Thomas Pock (optimisation, machine learning), and myself.

      Needed qualification: completed doctoral studies in computer science, software engineering or a comparable subject.

      Wanted qualifications:

      • Basic knowledge and research experience in one or more of the following areas:
        •  Model-based testing and test case generation
        •  Formal development methods (TLA+, Event-B, ...)
        •  Verification (Model Checking, Theorem Proving)
        •  Automata Learning (Model Inference)
        •  Symbolic execution
        • Testing/verification of machine learning components
        • Testing/verification of embedded systems
        • Testing/verification of temporal and stochastic systems
      • Successful thematically relevant publication activity
      • Interest in participating in teaching
      • Very good knowledge of English

      Application deadline: 30 Sep 2020.

      For further details and information how to apply, see: https://www.tugraz.at/fakultaeten/csbme/news/jobs-grants-calls/7160-20-036/

      A brief description of the DES Lab can be found on my homepage: https://aichernig.blogspot.com

      In case of questions, feel free to contact me via email: Bernhard Aichernig <aichernig@ist.tugraz.at>

      Wednesday, 29 January 2020

      New Research Lab: Dependable Embedded Systems Lab (DES Lab)

      I will manage a new research lab that has been launched by TU Graz and Silicon Austria Labs (SAL). The TU Graz - SAL Dependable Embedded Systems Lab (DES Lab) will carry out fundamental research in order to provide dependability of modern computer-based systems. Top computer scientists from TU Graz will be working here together with researchers from SAL on the development of new methods to make intelligent and networked systems more dependable (safety, security, availability, correctness, ...). To this end, the DES Lab will conduct interdisciplinary basic research in the areas of testing, verification, machine learning, optimisation and hardware-related software development with a special focus on security and dependability.

      Idea and Motivation. With recent advances in Internet connectivity, network enabled devices have become a substantial part of our everyday lives, extending into areas of increasing importance and criticality. Consequently, those systems must meet high standards with respect to dependability: Systems must be secure, safe, correct, reliable, maintainable, adaptable, and robust. However, these requirements for dependability are challenged by the growing complexity of modern embedded systems. On one hand, embedded systems are integrated into systems of systems that pool their resources and capabilities in order to offer more functionality and performance than simply the sum of its constituents. On the other hand, we face a paradigm shift towards more intelligent and highly adaptive systems where quality guarantees are hard to achieve. The opportunities seem unlimited, and yet these characteristics appear to be overwhelming in their complexity that any assurances of dependability seem out of reach. 
      1. Our answer to this problem is twofold: dependable embedded systems require rigor: the complexity has to be mastered by precise abstraction techniques that enable compositional specification and verification; 
      2.  smart embedded systems demand smart development methods: the complexity due to “intelligent” software has to be mastered by new "intelligent" and rigorous software and methods.
      The following researchers from TU Graz together with researchers from SAL will collaborate in the DES Lab: 

      Further information on the general idea behind the joint research labs can be found in the press release.

      Monday, 13 May 2019

      9 PhD Positions in "Dependable Internet of Things"

      I am hiring a PhD in Model-based Testing and Automata Learning as part of

      9 University Assistant Positions in "Dependable Internet of Things"
      Graz University of Technology, Austria

      The Excellence Research Center "Dependable Internet of Things in Adverse Environments" at Graz University of Technology (TU Graz) has been established in 2016 and has been extended until 2021 after a successful midterm evaluation. For further information see http://dependablethings.tugraz.at. The mission of this long-term center is to foster a highly interdisciplinary research team spanning the computer science and electrical engineering faculties to lay the scientific foundations for an Internet of Things that is highly reliable, safe, and secure in order to enable critical applications that require guaranteed performance and long-term operation even in adverse environments. The center is seeking to fill 9 University Assistant positions with excellent candidates, who will pursue their PhD working closely together in three sub-projects that focus on the following topics:

      1. Dependable Wireless Communication and Localization: one position in wireless networking (Institute for Technical Informatics), one position in physical layer signal processing (Signal Processing and Speech Communication Lab), and one position in tunable microwave frontends (Institute for Microwave and Photonic Engineering).

      2.  Verified Dependability by Design: one position in embedded security and one position in formal verification (both at Institute of Applied Information Processing and Communications), one position in real-time operating systems (Institute for Technical Informatics), one position in model-based testing (Institute for Software Technology).

      3. Dependable Multi-Agent Systems: one position in robotics (Institute for Software Technology), and one position in information and control theory (Signal Processing and Speech Communication Lab).

      Applicants must hold a Master degree (or equivalent) in computer engineering, computer science, electrical engineering, or a related field before they can take on the position. Proficiency in the English language (spoken and written) is required. Applicants should be highly motivated, take initiative and responsibility, be able to work independently and in an interdisciplinary team, should have interest in scientific research, be committed to publish research results and to obtain a doctoral degree (PhD).

      The positions are to be filled as soon as possible from July 2019 with an initial appointment for three years. Each position is remunerated according to the collective contract (Kollektivvertrag) for Austrian Universities, salary scale B1, the annual salary amounts to 40.103 EUR/year before taxes and may increase in case of relevant prior work experience.

      TU Graz aims to increase the number of female employees and therefore specifically invites qualified women to apply.

      TU Graz is a leading technical university in Austria (rank 75-100 in Shanghai subject ranking "Computer Science & Engineering") in a medium-sized city with a very high quality of life, located at the south-eastern foot of the Alps, offering plentiful recreation opportunities.

      Applicants should fill in the application form at http://dependablethings.tugraz.at/jobs and upload it together with a transcript of records, a copy of the master's degree, a recent certificate of the level of proficiency of the English language, a copy of the master's thesis, and any recommendation letter of your former advisor(s) at http://lampz.tugraz.at/~dependablethings/. The application deadline is 07.06.2019. The ID of this job post is 4480/19/010. For further information please contact the center coordinator Prof. Kay Roemer <roemer@tugraz.at>.

      Tuesday, 16 April 2019

      Professional Activities in 2019

      Here is a summary of my activities in 2019. This list will be updated as tasks come along.
      • Key Researcher in the project Dependable Things 
      • Invited speaker at UTP 2019, the 7th International Symposium on Unifying Theories of Programming, celebrating Tony Hoare's 85th birthday, Porto, Portugal, 8 Oct 2019.
      • Member of AVL's Strategic Research Partnership Program (AVL SRP), subtopic: Intelligent Cognitive Systems. 
      • Steering board member of TAP, the International Conference on Tests and Proofs
        • PC Member of 
          • FM 2019, 23rd International Symposium on Formal Methods
          • UTP 2019, 7th International Symposium on Unifying Theories of Programming
          • iFM 2019, 15th International Conference on integrated Formal Methods
          • FMICS2019, Formal Methods for Industrially Critical Systems
          • IFIP ICTSS 2019, 31st International Conference on Testing Software and Systems
          • ICFEM 2019, 21st International Conference on Formal Engineering Methods
          • A-MOST 2019, 15th Workshop on Advances in Model Based Testing
          • Refine 2019, Refinement Workshop
          • ITEQS 2019, 3rd International Workshop on Testing Extra-Functional Properties and Quality Characteristics of Software Systems
        • Guest Editor of the Wiley journal Software Testing, Verification and Reliability (STVR) for a special issue on Testing Extra-Functional Properties. 
        • Member of the selection boards for 
          • a full professorship in Information Security
          • a tenure track position in Cryptography
          • external master students in the programmes Computer Science and Software Engineering and Management
        • Teaching 
          • Quality Assurance in Software Development, 
          • Software Paradigms, 
          • Model-based Testing, 
          • Logic and Logic Programming, and 
          • Functional Programming.

        Thursday, 14 June 2018

        Professional Activities in 2018

        Here is a summary of my activities in 2018. This list will be updated as tasks come along.

        Tuesday, 4 July 2017

        New article on requirements modelling, model-based testing and traceability

        Our article on combining requirements modelling, test-case generation and traceability appeared in the Springer STTT journal.

        The paper describes how we
        1. model requirements as contracts in the form of assume-guarantee conditions 
        2. generate test cases efficiently out of the models via SMT solving and an incremental algorithm
        3. add traceability information linking requirements, contracts, generated test-cases and test results
        4. demonstrated its feasibility with our industrial partner Infineon on airbag electronics.  
        All of this comes with solid foundations and precise semantics.

        Bernhard K. Aichernig, Klaus Hörmaier, Florian Lorber, Dejan Nickovic, and Stefan Tiran. Require, test, and trace IT. International Journal on Software Tools for Technology Transfer (STTT), 19:409–426, 2017. Open Access. Published online: 29 November 2016. (PDF) (doi:10.1007/s10009-016-0444-z)

        It is open access and can be freely accessed at Springer.

        Enjoy!

        Thursday, 12 January 2017

        Professional Activities in 2017

        Here is a summary of my activities in 2017. This list will be updated as tasks come along.
        • Key Researcher in the projects 
        • Invited Speaker at the 11th Alpine Verification Meeting (AVM 2017),  Visegrad, Hungary, 18 - 21 Sep 2017.
        • Member of the appointment committee for the professorship in Information Security. 
        • External PhD examiner of Zhengkui Zhang, Aalborg University, Denmark. Thesis title: "Time and Cost Optimisation of Cyber-Physical Systems by Distributed Reachability Analysis". 
        • PC Member of 
          • A-MOST 2017, 13th Workshop on Advances in Model Based Testing
          • TAP 2017, 11th International Conference on Tests & Proofs
          • TASE 2017, 11th International Symposium on Theoretical Aspects of Software Engineering
          • MBT 2017, 11th Int. Workshop on Model-Based Testing
          • ICFEM 2017, 19th International Conference on Formal Engineering Methods
          • ICTAC 2017, 14th International Colloquium on Theoretical Aspects of Computing
        • Guest Editor of the Springer Journal Formal Aspects of Computing for a special issue of TAP 2016
        • Associate Editor of the open access journal Frontiers in ICT, section Formal Methods.
        • Teaching 
          • Quality Assurance in Software Development, 
          • Software Paradigms, 
          • Model-based Testing, 
          • Logic and Logic Programming, and 
          • Functional Programming.


        Wednesday, 19 October 2016

        New Journal Article on Test-Case Generation and Fault Propagation

        Our new article on fault propagation and its relation to model-based test-case generation was just published:

        Bernhard K. Aichernig, Elisabeth Jöbstl, and Martin Tappler. Does this fault lead to failure? Combining refinement and input-output conformance checking in fault-oriented test-case generation. Journal of Logical and Algebraic Methods in Programming, 85(5, Part 2):806–823, 2016. (PDF) (doi:10.1016/j.jlamp.2016.02.002)

        The publisher Elsevier provides a free download of the original article until December 2.

        The paper describes how we generate test-cases for reactive systems by

        1. injecting faults into the models (mutation testing)
        2. generating a test-case that triggers this fault (refinement checking)
        3. extending the test-case until an observational failure could be produced (ioco checking).

        We show that this is more efficient than previous approaches that search for observational equivalences directly, i.e. skipping Step 2.

        Our case study of a car-alarm controller shows that for some subtle faults we need up to nine additional interactions until a fault becomes visible at the interface.

        Friday, 5 August 2016

        Professional Activities in 2016

        I have been invited to serve on the PC of SVT 2017, the 32nd Annual ACM Symposium on Applied Computing Software Verification and Testing Track that will be held in Marrakech, Morocco, April 3 – 7, 2017.

         Here is a summary of my activities in 2016:

        Friday, 5 February 2016

        Designing Embedded Domain-Specific Languages in Scala

        I am glad to share with you an excellent Bachelor's thesis written by Philipp Gabler and supervised by me. The topic is fascinating as it discusses the features of the programming language Scala to support the design of DSLs. It includes a case-study on our modeling language for model-based testing.

        Philipp Gabler, Designing Embedded Domain-Specific Languages in Scala: a Case Study with Action Systems, Bachelor's Thesis, Graz University of Technology, Institute for Software Technology,  June 2015.

        Here is the PDF for download.

        Thursday, 22 October 2015

        10 PhD Positions in Dependable Internet of Things

        We have 10 PhD positions in my new project:

        Graz University of Technology (TU Graz) has recently established an
        Excellence Research Center entitled "Dependable Internet of Things
        in Adverse Environments", for further information see
        http://dependablethings.tugraz.at. The mission of this long-term
        center is to foster a highly interdisciplinary research team
        spanning the computer science and electrical engineering faculties
        to lay the scientific foundations for an Internet of Things that
        is highly reliable, safe, and secure in order to enable critical
        applications that require guaranteed performance even in adverse
        environments. The center is seeking to fill 10 PhD positions with
        excellent candidates, who will work closely together in four
        subprojects that focus on the following topics:

        1. Dependable Wireless Communication and Localization (three
           positions in wireless networking, physical layer signal
           processing, and tunable microwave frontends)

        2. Dependable Embedded Computing (two positions in embedded
           hardware and software with a focus on security and real-time
           operating systems)

        3. Dependable Composition of Smart Things (three positions in
           model checking, model-based testing, and machine learning)

        4. Dependable Networked Control (two positions in control theory
           and information theory)

        Applicants must hold a Master degree (or equivalent) in computer
        engineering, computer science, or electrical engineering before
        they can take on the position. Proficiency in the English language
        (spoken and written) is required. Applicants should be highly
        motivated, have initiative and responsibility, be able to work
        independently and in an interdisciplinary team, should have
        interest in scientific research, should have commitment to
        publish research results and to obtain a doctoral degree.

        The positions are to be filled from January 1, 2016 with an
        initial appointment for three years. The position is remunerated
        according to the collective contract (Kollektivvertrag) for
        Austrian Universities, i.e., the salary amounts to at least
        37.280 EUR/year before taxes and may increase depending on prior
        experience.

        TU Graz aims to increase the number of female employees and
        therefore specifically invites qualified women to apply.

        TU Graz is a leading technical university in Austria (ranking
        151-200 in the world in engineering in the Shanghai Ranking)
        in a medium-sized city with a very high quality of life,
        located at the south-eastern foot of the Alps, offering
        plentiful recreation opportunities.

        Applicants should fill in the application form at
        with a transcript of records, a copy of the master's degree,
        a recent certificate of the level of proficiency of the English
        language, and a copy of the master's thesis at
        The application deadline is November 30, 2015. For further
        information please contact the center coordinator Prof. Kay
        Roemer <roemer@tugraz.at>.

        Thursday, 20 August 2015

        Professional Activities in 2015

        The professional life of a researcher is exciting! Here are some of my activities in 2015:
        • PC Co-Chair of TAP 2016, the 10th International Conference on Tests & Proofs, July 2016,Vienna, Austria.
        • Associate Editor of the new open access journal Frontiers in ICT, section Formal Methods 
        • Presentation at FMICS 2015Require, Test and Trace IT
        • Presentation at Festschrift Symposium in Honor of Jose Nuno Oliveira, Guimaraes, Portugal, 26 Sep 2015: Does this Fault Lead to Failure? Combining Refinement and Input-Output Conformance Checking in Fault-Oriented Test-Case Generation.
        • Co-Organizer of the Doctoral Symposium of Formal Methods 2015
        • Invited tutorial at SQAMIA 2015: Killing Bugs in a Black Box with Model-based Testing: from Science via Tool Development to Industrial Application
        • Key Researcher in the Dependable Things project
        • Key Researcher in the TRUCONF project
        • Key Researcher in the CRYSTAL project
        • PC Member and Publicity Chair of ICST 2015
        • PC Member of FM 2015
        • PC Member of MBT 2015
        • PC Member of SEFM 2015
        • PC Member of TAP 2015
        • Reviewer for the journals Formal Aspects of ComputingScience of Computer Programming,  Logical and Algebraic Methods in Programming, and Information and Software Technology.
        • Board Member of Formal Methods Europe
        • Chair of the Study Commission for the studies Computer Science, Software Development and Business Management, and the Teacher Learning Programme Computer Science at TU Graz
        • Voting Member of the Selection Commission for Admission to the Master's Program in Computer Science at TU Graz
        • Teaching Quality Assurance in Software Development (84 students)
        • Teaching Software Paradigms (263 students)
        • Teaching Model-based Testing (24 students)
        • Teaching Logic and Logic Programming (170 students)
        • Teaching Functional Programming (149 students)

        Monday, 17 November 2014

        New journal article on model-based testing

        Today, our new journal article appeared in the Science of Computer Programming journal of Elsevier.

        It deals with the problem of automatically generating test-cases from mutated models:

        Bernhard K. Aichernig, Elisabeth Jöbstl, and Stefan Tiran. Model-based mutation testing via symbolic refinement checking. Science of Computer Programming. 97 (2015): 383-404, Elsevier, 2015.

        Here is a link to a free copy of it that works for 50 days.

        Highlights:

        • We deal with model- and mutation-based test case generation.
        • The main focus lies on optimizations of the underlying conformance check.
        • We explain the construction of test cases based on the conformance check.
        • We allow for non-determinism in the test models.
        • We demonstrate the effectiveness of our optimizations on industrial case studies.

        Enjoy!