Linkedin

Verification and Software Engineering

Contributing key researchers: 
Kim G. Larsen (AAU)
Hanne Riis Nielson (DTU)
Andrzej Wasowski (ITU)
Thomas Hildebrandt (KU)
Peter Schneider-Camp (SDU)

Kim Guldstrand Larsen
Professor


Aalborg University
Department of Computer Science
Selma Lagerlöfsvej 300
9220 Aalborg Ø

E: kgl@cs.aau.dk
T: +45 99 40 88 93
LINKEDIN
WS7

Relevance

The growing pervasiveness of computerised systems makes our society extremely vulnerable to faults or attacks to such systems. Here rigorous software engineering methods and supporting efficient verification tools are crucial to counter this threat of complexity. In addition, the growing number of software components that are based on ”unexplainable” and ”on-line” machine learning components possess a particular future challenge for verification research.

The growing use of personal data in software systems in the public as well as private sector gives rise to new challenges in verification and software engineering in guaranteeing privacy-by-design. Finally, the pervasive use of business process and case management systems in domains regulated by law, such as financial and governmental services, puts high demands for verification and software engineering technologies for compliance in general.

Objectives and Synergies

The objectives are

  1. to develop rich mathematically rigorous modelling and analysis frameworks for the behaviour of complex distributed software systems. The frameworks should allow functional correctness, resource efficient and security aspects – as well as their tradeoffs – to be captured and analysed,

  2. to develop and implement supporting verification and analysis tools that scale to the growing complexity software systems, and

  3. transfer of frameworks and tools into industrially used development practice.

The research within Verification and Software Engineering complements and exploits techniques from other research themes. In particular, verification may be applied establish security properties of Secure Multiparty Computations of Blockchains as found in the Cybersecurity and Blockchain theme as already demonstrated by the Center for Program Verification. The dependability and robustness of several CPS and IoT-based systems may be established by Verification and Software Engineering methods.

Artificial Intelligence is increasingly exploited to accelerate and scale current verification techniques. Dually, machine-learned components, such as Deep Neural Networks, are challenging existing algorithmic techniques for verification with exciting research emerging these days towards verifiable and explainable AI.