Research Topics

Contents

 

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.

                      Co-funded by the European Union