Automated Software Analysis Group

Welcome to Automated Software Analysis Group!

The Automated Software Analysis (ASA) group, led by Junior Prof. Dr. Mana Taghdiri, is a part of the Institute for Theoretical Computer Science at the Department of Informatics in Karlsruhe Institute of Technology (south campus). This research group focuses on improving the reliability of software systems by developing automatic techniques that increase programmers' confidence in their developed systems. We statically check the correctness of software systems both at the algorithm/design levels and also program/implementation levels. We target structure-rich software such as network protocols or object-oriented programs that extensively manipulate data structures.

Similar to other static analysis techniques, scalability to large systems is our major challenge. We investigate different ideas to make our analyses scalable, while keeping them fully automatic, practical, and easy to use. In addition to developing general program analysis techniques, we study what problems arise in different domain-specific applications, and investigate how our techniques can be adapted to such domains. Examples include software security, routing libraries, network protocols, and numerical software.

Our broad areas of research are software engineering and formal methods, and include:

  • Bounded verification of object-oriented code (see our InspectJ page),
  • Checking design-level requirements,
  • Sepcification extraction from code,
  • Formal specification languages,
  • Constraint solver development (see our AlloyPE and Kelloy pages),
  • Software testing and debugging