# Research Topics

Contents

- 1
- 2 Research Topic 1: Symbolic Computation for Loop Analysis
- 3 Research Topic 2: Computational Argumentation
- 4
- 5 Research Topic 3: Parameterized Complexity of Problems in Artificial Intelligence
- 6 Research Topic 4: Fixed-Parameter Algorithms by Exploiting the Structural Properties of Inputs
- 7 Research Topic 5: Analysis/Synthesis of Probabilistic Programs
- 8 Research Topic 6: Verification of Hyperproperties
- 9 Research Topic 7: Learning Requirements
- 10 Research Topic 8: Normative Reasoning for Autonomous Systems
- 11 Research Topic 9: Computer Search in Discrete Mathematics
- 12 Research Topic 10: Formal Methods in Computational Social Choice
- 13 Research Topic 11: SAT-Based Methods for Explainable Al
- 14 Research Topic 12: Formal Methods for Security and Privacy
- 15 Research Topic 13: Normative reasoning: from Ancient Texts to Artificial Intelligence
- 16 Research Topic 14: Ethical Reasoning in Cyberphysical Systems: Combining Logic and Machine Learning
- 17 Research Topic 15: Proof Theory & Automated Deduction for Non-Classical Logics
- 18 Research Topic 16: Deontic ASP
- 19 Research Topic 17: Formal Methods for Testing and Bug Finding
- 20 Research Topic 18: Model Checking and Satisfiability Solving
- 21 Research Topic 19: Automated Resource Bound Analysis
- 22 Research Topic 20: Verification of Pointer-Manipulating Programs
- 23 Research Topic 21: Verification of Concurrent and Distributed Systems
- 24 Research Topic 22: Numeric Reasoning in DLs
- 25 Research Topic 23: Domain Ontologies for Explainable AI
- 26 Research Topic 24: Distributed Stream Reasoning
- 27 Research Topic 25: Hybrid Answer Set Programming
- 28 Research Topic 26: Abductive Reasoning for Explainable Scheduling
- 29 Research Topic 27: Multi-objective contextual reasoning

### Research Topic 1: Symbolic Computation for Loop Analysis

**PI/Supervisor: Laura Kovacs
**The project will focus on developing symbolic computation algorithms for the analysis of program loops with numeric and unbounded data structures, as well as probabilistic features. For doing so, computer algebra techniques in combination with statistical method will be designed to analyze safety and liveness properties of emerging applications of programming languages.

### Research Topic 2: **Computational Argumentation**

**PI/Supervisor: Stefan Woltran**

### Research Topic 3: **Parameterized Complexity of Problems in Artificial Intelligence**

**PI/Supervisor: Robert Ganian
**The project will focus on obtaining an in-depth understanding of the parameterized complexity of prominent problems that arise in artificial intelligence research and in related areas. The pursued topics and general approaches may, for instance, follow a similar direction as the following recent publications: [1] Robert Ganian, Sebastian Ordyniak: The complexity landscape of decompositional parameters for ILP. Artif. Intell. 257: 61-71 (2018). [2] Robert Ganian, Thekla Hamm, Guillaume Mescoff: The Complexity Landscape of Resource-Constrained Scheduling. IJCAI 2020: 1741-1747.

### Research Topic** 4: Fixed-Parameter Algorithms by Exploiting the Structural Properties of Inputs**

**PI/Supervisor: Robert Ganian
**The project will target new fixed-parameter algorithms and algorithmic lower bounds for fundamental problems in theoretical computer science. The focus will lie on techniques that utilize structural parameters of an input graph. Example papers: [1] Robert Ganian, Fabian Klute, Sebastian Ordyniak: On Structural Parameterizations of the Bounded-Degree Vertex Deletion Problem. Algorithmica 83(1): 297-336 (2021) [2] Eduard Eiben, Robert Ganian, Thekla Hamm, Fabian Klute, Martin Nöllenburg: Extending Partial 1-Planar Drawings. ICALP 2020: 43:1-43:19

### Research Topic** 5: Analysis/Synthesis of Probabilistic Programs**

**PI/Supervisor: Ezio Bartocci**

### Research Topic **6: Verification of Hyperproperties**

**PI/Supervisor: Ezio Bartocci**

### Research Topic **7: Learning Requirements**

**PI/Supervisor: Ezio Bartocci**

### Research Topic **8: Normative Reasoning for Autonomous Systems**

**PI/Supervisor: Ezio Bartocci**

### Research Topic **9: Computer Search in Discrete Mathematics**

**PI/Supervisor: Stefan Szeider**

There are many open problems in Discrete Mathematics, including Extremal Graph Theory, Ramsey Theory, and Design Theory, where one is interested in finding smallest examples or counterexamples to conjectures. Since the search space grows quickly with the size of the objects, advanced symmetry-breaking methods are essential. This project combines symmetry-breaking with SAT-based methods. Relevant literature: [1] Michael Codish, Alice Miller, Patrick Prosser, Peter J. Stuckey: Constraints for symmetry breaking in graph representation. Constraints, an Int. J. 24(1): 1-24 (2019). [2] Tomás Peitl, Stefan Szeider: Finding the Hardest Formulas for Resolution. CP 2020: 514-530.

### Research Topic **10: Formal Methods in Computational Social Choice**

**PI/Supervisor: Stefan Szeider**

This project aims to utilize recent SAT-solving progress to tackle problems that arise in Computational Social Choice, such as the aggregation of preferences of multiple agents or the prevention of rigged elections. The work includes theoretical investigations combined with experimental evaluation on real-world data. Relevant literature: [1] Ulle Endriss: Analysis of One-to-One Matching Mechanisms via SAT Solving: Impossibilities for Universal Axioms. AAAI 2020: 1918-1925. [2] André Schidler, Stefan Szeider: SAT-based Decision Tree Learning for Large Data Sets. AAAI 2021: 3904-3912.

### Research Topic **11: SAT-Based Methods for Explainable Al**

**PI/Supervisor: Stefan Szeider**

This project analyzes subsymbolic machine learning models, such as neural networks, with symbolic tools like SAT solvers. The aim is to replace opaque models with explainable and verifiable models, easily checked for bias. Relevant literature: [1] Alexey Ignatiev, Nina Narodytska, João Marques-Silva: Abduction-Based Explanations for Machine Learning Models. AAAI 2019: 1511-1519. [2] Christoph Molnar: Interpretable machine learning. A Guide for Making Black Box Models Explainable, 2019. https://christophm.github.io/interpretable-ml-book/. [3] André Schidler, Stefan Szeider: SAT-based Decision Tree Learning for Large Data Sets. AAAI 2021: 3904-3912.

### Research Topic **12: Formal Methods for Security and Privacy**

**PI/Supervisor: Matteo Maffei**

### Research Topic **13: Normative reasoning: from Ancient Texts to Artificial Intelligence**

**PI/Supervisor: Agata Ciabattoni**

Norms are enormously important in a variety of fields, including law, emergency management and AI. The application of norms inevitably leads to deontic conflicts and deciding which norms override which other norms is often controversial. This project investigates conflict resolution methods for normative reasoning and aims to develop effective tools usable in application domains. As our main source of inspiration, we look at ways of dealing with normative reasoning that diverge from the contemporary European and Anglo-American approaches, thereby questioning implicit cultural biases in dealing with deontic conflicts. The various legal and philosophica ltraditions we will examine will be applied to real-world reasoning scenarios coming from contemporary ethical debates and normative AI cases.

### Research Topic **14: Ethical Reasoning in Cyberphysical Systems: Combining Logic and Machine Learning**

**PI/Supervisor: Agata Ciabattoni**

### Research Topic **15: Proof Theory & Automated Deduction for Non-Classical Logics**

**PI/Supervisor: Agata Ciabattoni**

### Research Topic **16: Deontic ASP**

**PI/Supervisor: Agata Ciabattoni**

### Research Topic **17: Formal Methods for Testing and Bug Finding**

**PI/Supervisor: Georg Weissenbacher**

Software and hardware is widely acknowledged to be full of bugs. Despite decades-long efforts, formal verification hasn’t fufilled the promise of providing us with correct-by-construction or provenly correct systems. Hence, this project focuses on formal falsification: automated testing and the automated detection of bugs in software and hardware. We target a broad range of bugs, including bugs in concurrent and distributed systems, security bugs, but also bugs in machine learning-based systems. The goal is to provide automated techniques that provide formal guarantees.

### Research Topic **18: Model Checking and Satisfiability Solving**

**PI/Supervisor: Georg Weissenbacher**

Model Checking is a technique to automatically check whether a given system (model) satisfies a property. Model checking has been successfully applied to hardware as well as software. Many successful model checking algorithms are based on satisfiability solvers, taking advantage of the huge strides made in this field in the last two decades. This project focuses on the tight integration and similarities of contemporary model checking algorithms and satisfiability solvers, exploiting and lifting the latest and most promising advances in automated solving to model checking.

### Research Topic **19: Automated Resource Bound Analysis**

**PI/Supervisor: Florian Zuleger**

Determining the resource consumption of a program (e.g., runtime, heap usage) is an integral part during the design and analysis of a program. In this project we are interested in static analysis techniques that allow deriving upper bounds on the resource consumption of a program. Techniques of interest include ranking functions, potential functions, program invariants, Hoare logic, assume-garantuee reasoning, etc. Further we are interested in decidabilty results on the resource consumption of foundational computing models such as Petri nets and counter automata.

### Research Topic **20: Verification of Pointer-Manipulating Programs**

**PI/Supervisor: Florian Zuleger**

Data structures in imperative programs are typically manipulated via pointers. The verification of such programs requires adequate logics that allow describing the shape and the current state of the data structure. In order to automate reasoning we are intersted in logics with decidable satisfiability and entailment problems. In this project we will study suitable logics, such as separation logic, and develop automated decision procedures. Moreover, we are intersted in static analysis techniques that derive program invariants, expressed in the considered logics, fully-automatically.

### Research Topic **21: Verification of Concurrent and Distributed Systems**

**PI/Supervisor: Florian Zuleger**

Present day computing witnesses a swift change of view between a single program running on a computer to a complex system, such as a cloud, an autonomous car or a cryptocurrency. This project aims at providing logical tools for the design and verification of such systems, using the principle of local reasoning: a state change, either internal or a reconfiguration, involves a limited resource, the rest of the system remaining unchanged. We plan to design logics for reasoning about such reconfigurable systems and automate these logics by new (semi-)decision procedures integrated with compositional push-button verification methods, that guarantee behavioral correctness.

### Research Topic **22: Numeric Reasoning in DLs**

**PI/Supervisor: Magdalena Ortiz**

Description Logics (DLs) are a versatile family of languages for knowledge representation, with efficient automated reasoning engines and many succesful applications. However, state-of-the-art technologies have extremely limited capabilties to reason with numeric values. As the latter are crucial in many potential applciations, major research efforts have aimed at enriching DLs with the ability to associate numeric values to logical objects (e.g., by the so called concrete domains), and to express numeric constraints both on such values and on the sizes of the extensions of classes and relations. Many promising solutions are emerging, but so far research is dominated by techniques that are good for establishing decidablity and complexity results, but poorly suited as the basis of such implementations. The goal of this project is to develop novel algorithms that can underpin DL engines with numeric reasoning support, mostly by translations into formalisms with efficeint solvers like integer linear programming and satisfiability module theories.

### Research Topic **23: Domain Ontologies for Explainable AI**

**PI/Supervisor: Magdalena Ortiz**

The urgency of accurate yet interpretable ML classifiers has resulted in many techniques for approximating and explaning systems by means of decision rules, decision trees, and similar interpretables model classes. Some of these approximation techniques use ad-hoc domain ontologies and very simple ontological reasoning to guide the constrcution of these explainable models, for example, to prioritize more informative features over less informative ones. This project will contribute to understanding the limits and possibilities of extracting knowledge from existing ontologies and using it to improve explainable classifiers.

### Research Topic **24: Distributed Stream Reasoning**

**PI/Supervisor: Thomas Eiter**

Stream reasoning is a topic of growing importance. It is in partciular challenging if multiple entities (agents) have to process and to exchange information resulting in streams, and if real-time settings play a role. While some proposals for semantics of systems of entities agents exist, there is room for improvement to take various features (numeric uncertainy, realibility, learning) etc. into account, in particular, if declarative methodes are used for describing the behaviour of the entities.

### Research Topic **25: Hybrid Answer Set Programming**

**PI/Supervisor: Thomas Eiter**

Answer Set Programming is a successful declarative problem solving paradigm that has been deployed to many application fields. In order to enlarge its applicability, Answer Set Programming has been extended and combined with other problem solving methods, among them SAT and SMT solving, imperative programming, constraint programming etc. Recently, there has been a strong interest in combining Answer Set Programming with Machine Learning, leading to neuro-symbolic computation models that integrate neural networks with rules, or apply reinfocement learning to rules and program evalution, or use Answer Set Programming to guide learning. In this project, the Hybrid ASP approach will be further extended, and novel integration, algorithms, and applications will be considered.

### Research Topic **26: Abductive Reasoning for Explainable Scheduling**

**PI/Supervisor: Thomas Eiter**

### Research Topic **27: Multi-objective contextual reasoning**

**PI/Supervisor: Thomas Eiter**

**Funding **

This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 101034440.