Logic and Formal Verification

Logic and Formal Verification

How can the correctness of software and hardware be formally verified? How can database queries be answered quicker? How can knowledge be stored so that it can be easily used? Formal methods from the field of logic play a major role in answering such questions.

Focus areas

The research area Logic and Formal Verification around Prof. Dr. Thomas Zeume applies logical methods to problems in computer science. Efficient algorithms for logics appearing in applications are developed and the expressiveness of such logics is studied.

efficient query evaluation for dynamic databases: extracting information from vast amounts of data that is frequently updated is a major challenge in many disciplines. Dynamic complexity theory studies the theoretical foundations of logical query languages for databases that are subject to frequent change. One of the main goals in this area is to develop a theory for classifying queries in terms of the amount of resources needed for their dynamic evaluation.

  • The research is concerned with the development of methods to study resource requirements for maintaining requests in dynamic contexts.

logic for specification and verification: the automated verification of software and hardware is an important task. Often, intended properties of a system are specified by logical formalisms. Similar formalisms are the basis for query languages to extract information from tree-like data and graph databases.

  • The team studies logical systems with respect to their applicability as specification and verification languages.

web-based teaching in the area of formal methods: a typical application of logic in computer science is modeling scenarios using logical formulas and inferring new knowledge from such modeling.

  • An interactive, web-based teaching system is being developed to support students in learning the necessary formal fundamentals.