Research Projects
[About  Programme  Training  Supervisors  Projects  Apply  Calls  Team  Student Guide  FAQ]
Research Project 1: Symbolic Computation for Loop Analysis 
PI/Supervisor: Laura Kovacs
Show More 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, such as synthesizing probabilistic loops from the value distributions of program variables and inferring tight bounds on the expected runtimes of probabilistic programs. 
Research Project 2: Computational Argumentation 
PI/Supervisor: Stefan Woltran
Show More Preferences are a crucial element in formalisations of argumentation scenarios. In this project, we aim to incorporate a recently proposed general framework for preference handling [1] to argumentation formalisms. Such preferences can be applied at different points in the evaluation process: one approach would be to rank outcomes of argumentation frameworks; another app roach is to rank possible completions of incomplete argumentation frameworks [2].
[1] Michael Bernreiter, Jan Maly, Stefan Woltran: Choice Logics and Their Computational Properties. Accepted for IJCAI’21. 
Research Project 3: Foundations of Logic Programming 
PI/Supervisor: Stefan Woltran
Show More Notions of equivalence between logic programs constitute central a theoretical tool to understand concepts like program simplification. While several such notions have been studied in the literature (e.g., [1]), recent developments like forgetting [2] or abstraction call for refined notions of equivalence. The overall goal in this project to define such notions and explore suitable logical characterisations.
[1] Stefan Woltran: A common view on strong, uniform, and other notions of equivalence in answerset programming. Theory Pract. Log. Program. 8(2): 217234 (2008) 
Research Project 4: Parameterized Complexity of Problems in Artificial Intelligence 
PI/Supervisor: Robert Ganian
Show More The project will focus on obtaining an indepth 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: 6171 (2018). 
Research Project 5: FixedParameter Algorithms by Exploiting the Structural Properties of Inputs 
PI/Supervisor: Robert Ganian
Show More The project will target new fixedparameter 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: 
Research Project 6: Analysis/Synthesis of Probabilistic Programs 
PI/Supervisor: Ezio Bartocci
Show More Probabilistic programs (PPs) are now gaining momentum due to the several emerging applications in the areas of machine learning and artificial intelligence. Hightech giants, such as Google, Microsoft and Uber, have started to develop their own probabilistic programming languages that include native constructs for sampling distributions, enabling the programmer to freely mix deterministic and stochastic elements. This programming paradigm offers a unifying framework for encoding probabilistic machine learning models, such as Bayesian networks, with decision making routines used, for example, in autonomous parking. One of the main problems that arise from introducing randomness into the program is that we can no longer view variables as single values, but as distributions of values. Dealing with distributions is far more complex and some simplifications and approximations are necessary. The resulting flexible framework comes at the price of programs with behaviors hard to analyze, leading to unpredictable consequences in safetycritical applications, such as in autonomous driving. This research project consists in developing new automated techniques to analyse probabilistic programs (e.g. proving termination, learning invariants, verifying safety condition) or to automatically synthesize probabilistic programs satisfying certain properties.
Preliminary work of the supervisors: 
Research Project 7: From Failure Explanation to Repair in CyberPhysical Systems 
PI/Supervisor: Ezio Bartocci
Show More Debugging CyberPhysical Systems (CPS) is a cumbersome and costly activity. CPS models combine continuous and discrete dynamics. A fault in a physical component manifests itself in a very different way than a fault in a state machine. Furthermore, faults can propagate both in time and space before they can be detected at the observable interface of the model. In recent work we have investigated fault localization [1] and failure explanation techniques [2] for Simulink/Stateflow diagrams of cyberphysical systems. The main idea of our approach is to combine testing [3], specification mining [4,5], and failure analysis to automatically explain failures supporting the debugging activities. This research project aims at further developing these techniques and going beyond them by automatically proposing possible repair solutions to the engineer.
[1] E. Bartocci, T. Ferrère, N. Manjunath, D. Nickovic: Localizing Faults in Simulink/Stateflow Models with STL. Proc. of HSCC 2018: 197206, doi: 10.1145/3178126.3178131 
Research Project 8: Verification of Probabilistic Hyperproperties 
PI/Supervisor: Ezio Bartocci
Show More Hyperproperties extend the conventional notion of trace properties from a set of traces to a set of sets of traces. Many interesting requirements in computing systems are hyperproperties and cannot be expressed by trace properties. Examples include (1) a wide range of informationflow security policies such as noninterference and observational determinism (2) sensitivity and robustness requirements in cyberphysical systems and consistency conditions such as linearizability in concurrent data structures. Hyperproperties can describe the requirements of probabilistic systems as well. They generally express probabilistic relations between multiple executions of a system. For example, in informationflow security, adding probabilities is motivated by establishing a connection between information theory and information flow across multiple traces. A prominent example is probabilistic schedulers that open up an opportunity for an attacker to set up a probabilistic covert channel. Or, probabilistic causation compares the probability of occurrence of an effect between scenarios where the cause is or is not present. This research project aims at developing new automated and possibly scalable exact or approximate techniques to verify probabilistic hyperproperties over different classes of probabilistic models ranging from Markov Decision Processes to Stochastic games.
Previous work of the supervisor: 
Research Project 9: Normative Reasoning for Autonomous Systems 
PI/Supervisors: Ezio Bartocci, Agata Ciabattoni
Show More Autonomous agents must possess the ability to adapt to (potentially unpredictable) changes in their environment. Machine learning techniques such as reinforcement learning (RL) haven proven successful methods for teaching agents this behaviour. However, when supporting humans, AI agents should restrict their own action to the ethical standards recognized in fundamental right and ethical theories, introducing a requirement for ethical reasoning. RL has been employed to enforce such standards as well; agents can be trained to act in line with further rewards/penalties assigned according to the performance of ethical/unethical behaviour through a reward function. However, this does not provide a guarantee of the desired behaviour. Moreover, such techniques are not well equipped to handle the complexities of ethical reasoning. In general, like other blackbox machine learning methods, RL cannot transparently explain why a certain policy is compliant or not. Additionally, when the ethical values are embedded in the learning process, a small change in their definition would require us to retrain the policy from scratch. This project aims at investigating how to embed normative reasoning techniques with the machine learning components responsible for the decision making, thus combing symbolic and subsymbolic AI.
[1] Emery Neufeld, Ezio Bartocci, Agata Ciabattoni, Guido Governatori: A Normative Supervisor for Reinforcement Learning Agents. CADE 2021: 565576, doi: 10.1007/9783030798765_32 
Research Project 10: Computer Search in Discrete Mathematics 
PI/Supervisor: Stefan Szeider
Show More 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 symmetrybreaking methods are essential. This project combines symmetrybreaking with SATbased methods.
Relevant literature: 
Research Project 11: Formal Methods in Computational Social Choice 
PI/Supervisor: Stefan Szeider
Show More This project aims to utilize recent SATsolving 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 realworld data.
Relevant literature: 
Research Project 12: SATBased Methods for Explainable Al 
PI/Supervisor: Stefan Szeider Show More 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: 
Research Project 13: Speeding up Algorithms with Machine Learning 
PI/Supervisor: Stefan Szeider Show More Many computational problems that arise in Artificial Intelligence and Combinatorial Optimization are intractable. Nevertheless, efficient, practical algorithms have been developed that exploit the hidden structure of problem instances that arise from realworld applications. This project aims at utilizing recent progress in Machine Learning to speed up such solving algorithms.
Relevant literature: 
Research Project 14: Formal Methods for Security and Privacy 
PI/Supervisor: Matteo Maffei
Show More Proofs of security and privacy are extremely complex and error prone and the most popular protocols, applications, and services are regularly affected by bugs and vulnerabilities. This state of affairs calls for the design of formal methods for the enforcement of rigorous security and privacy properties in complex, large scale systems. A central challenge in this field is to strive for the sweet spot between automation and expressiveness. Target application domains include web applications, smart contracts, blockchain protocols, and learningbased systems.
[1] EThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. Schneidewind, Grischchenko, Scherer, Maffei. ACM CCS’20: 621640 
Research Project 15: Normative reasoning: from Ancient Texts to Artificial Intelligence 
PI/Supervisor: Agata Ciabattoni
Show More 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 AngloAmerican approaches, thereby questioning implicit cultural biases in dealing with deontic conflicts. The various legal and philosophica ltraditions we will examine will be applied to realworld reasoning scenarios coming from contemporary ethical debates and normative AI cases.

Research Project 16: Proof Theory for NonClassical Logics 
PI/Supervisor: Agata Ciabattoni
Show More Logics different from classical logics (Non classical logics) provide adequate formalisms for reasoning, e.g., about time, norms, knowledge, dynamic data structures, vague information and resources. As such, these logics have been increasingly applied in various disciplines including artificial intelligence, philosophy, and in computer science, where most of these logics originate.
Non classical logics are usually introduced or described in a declarative way in the proof framework due to Hilbert and Frege. However, the resulting systems are extremely cumbersome when it comes to finding or analyzing proofs and for proving properties of the formalized logics. These tasks call for algorithmic presentations of the logics especially in the form of analytic calculi. Analyticity is crucial here since proofs in such calculi proceed by a stepwise decomposition of the objects to be proved. The aim of this project is to advance the methods for the automated introduction of analytic calculi for nonclassical logics, and their exploitation. 
Research Project 17: Foundations for Normative Reasoning for AI Systems 
PI/Supervisor: Agata Ciabattoni
Show More The interpretation and application of norms have traditionally been the reserve of law and morality. Both of these areas have developed a number of methods, which are often not formally specified. Recently, especially in connection with the growth of Artificial Intelligence (AI) which is making autonomous systems mainstream, norms have become of central interest also for formal disciplines such as Logic and Computer Science.
As the real word is not predictable and unforeseen situations might arise,AI systems should be equipped with the ability to reason with and about norms. The aim of this project is to provide novel methods to achieve that, i.e., methods that will enable AI systems to comply not only with precise legal rules and deal with explicit exceptions, but also to reflect upon rules, assessing the impact of the rulesʼ application on the relevant values and provide appropriate corrections. 
Research Project 18: Formal Methods for Testing and Bug Finding 
PI/Supervisor: Georg Weissenbacher Show More Software and hardware is widely acknowledged to be full of bugs. Despite decadeslong efforts, formal verification hasn’t fufilled the promise of providing us with correctbyconstruction 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 learningbased systems. The goal is to provide automated techniques that provide formal guarantees. 
Research Project 19: Model Checking and Satisfiability Solving 
PI/Supervisor: Georg Weissenbacher
Show More 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 Project 20: Automated Resource Bound Analysis 
PI/Supervisor: Florian Zuleger
Show More 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, assumegarantuee 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 Project 21: Verification of PointerManipulating Programs 
PI/Supervisor: Florian Zuleger
Show More 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, fullyautomatically. 
Research Project 22: Verification of Concurrent and Distributed Systems 
PI/Supervisor: Florian Zuleger Show More 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 pushbutton verification methods, that guarantee behavioral correctness. 
Research Project 23: Numeric Reasoning in DLs 
PI/Supervisor: Magdalena Ortiz Show More Description Logics (DLs) are a versatile family of languages for knowledge representation, with efficient automated reasoning engines and many succesful applications. However, stateoftheart 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 Project 24: Domain Ontologies for Explainable AI 
PI/Supervisor: Magdalena Ortiz
Show More 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 adhoc 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 Project 25: Distributed Stream Reasoning 
PI/Supervisor: Thomas Eiter
Show More 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 realtime 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 Project 26: Hybrid Answer Set Programming 
PI/Supervisor: Thomas Eiter Show More 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 neurosymbolic 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 Project 27: Abductive Reasoning for Explainable Scheduling 
PI/Supervisor: Thomas Eiter
Show More Symbolic formalisms, among them mixed integer programming, constraint solving, SAT solving and answer set programming, have been successfully used for describing and solving scheduling problems in different applications domains. However, the (non)existence of solutions is not always clear, and in case of optimization aspects that may lead to (non)optimality. Abduction is a wellknown mechanism in order to find explanations of unexpected observations. In this project, the use of abduction for making scheduling results more explainable to users will be explored. 
Research Project 28: Multiobjective contextual reasoning 
PI/Supervisor: Thomas Eiter
Show More Drawing inferences and conclusions in general depends on the context in which a reasoner is situated; e.g., cheering to a goal of your team is natural in general, but may be inappropriate if you are in the stadium among hooligans favouring the opponents. Dealing with context often requires to deal with ambiguity and possibly overriding of information due to inheritance from more general to specific settings. Furthermore, contexts might come in different aspects, like time, space etc. (above, when we are watching a match, and where). This project will explore challenges that come from such a setting, which leads to multiobjective optimisation problems. A possible starting point are contextknowledge repositories, which are a versatile formalisms based on description logics. In particular, providing semantics, studying complexity of inference (which besides classical query answering might also include whatif questions), developing efficient algorithms and addressing applications would be on the agenda. 
Funding
This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie SkłodowskaCurie
grant agreement No 101034440.