Research Projects
[About | Programme | Training | Supervisors | Projects | Apply | Calls | Team | Student Guide | FAQ]
Available Projects:
Research Project: Verification of Pointer-Manipulating 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, fully-automatically. |
Filled/Unavailable Projects:
Research Project: 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: Parameterized Complexity of Problems in Artificial Intelligence |
PI/Supervisor: Robert Ganian
Show More 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). |
Research Project: Fixed-Parameter Algorithms by Exploiting the Structural Properties of Inputs |
PI/Supervisor: Robert Ganian
Show More 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: |
Research Project: 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. High-tech 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 safety-critical 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: From Failure Explanation to Repair in Cyber-Physical Systems |
PI/Supervisor: Ezio Bartocci
Show More Debugging Cyber-Physical 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 cyber-physical 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: 197-206, doi: 10.1145/3178126.3178131 |
Research Project: 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 information-flow security policies such as noninterference and observational determinism (2) sensitivity and robustness requirements in cyber-physical 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 information-flow 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: 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 black-box 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 sub-symbolic AI.
[1] Emery Neufeld, Ezio Bartocci, Agata Ciabattoni, Guido Governatori: A Normative Supervisor for Reinforcement Learning Agents. CADE 2021: 565-576, doi: 10.1007/978-3-030-79876-5_32 |
Research Project: Formal Methods for Security and Privacy |
PI/Supervisor: Matteo Maffei
[1] EThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts. Schneidewind, Grischchenko, Scherer, Maffei. ACM CCS’20: 621-640 |
Research Project: 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 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 Project: 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 real-world applications. This project aims at utilizing recent progress in Machine Learning to speed up such solving algorithms.Relevant literature: [1] Yoshua Bengio, Andrea Lodi, Antoine Prouvost: Machine learning for combinatorial optimization: A methodological tour d’horizon. Eur. J. Oper. Res. 290(2): 405-421 (2021) [2] Jia Hui Liang, Vijay Ganesh, Pascal Poupart, Krzysztof Czarnecki: Learning Rate Based Branching Heuristic for SAT Solvers. SAT 2016: 123-140 [3] Holger H. Hoos, Tomás Peitl, Friedrich Slivovsky, Stefan Szeider: Portfolio-Based Algorithm Selection for Circuit QBFs. CP 2018: 195-209 |
Research Project: 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 Project: 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 push-button verification methods, that guarantee behavioral correctness. |
Research Project: 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 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 Project: 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 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 Project: 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, such as assigning jobs to machines, assembling a roster for nurses in a hospital, etc.
However, the (non)existence of solutions is not always clear, why certain assignments are made (or not), why certain candidate schedules are not acceptable, or in case of optimization why they are not optimal etc. This project aims to research on methods and tools for answering these questions in terms of meaningful explanations that refer to data or statements in the problem description, providing valuable support to the user for obtaining more insight into a scheduling problem. |
Research Project: Multi-objective 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 multi-objective optimisation problems. A possible starting point are context-knowledge 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 what-if questions), developing efficient algorithms and addressing applications would be on the agenda. |
Research Project: 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: 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 answer-set programming. Theory Pract. Log. Program. 8(2): 217-234 (2008) |
Research Project: 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 symmetry-breaking methods are essential. This project combines symmetry-breaking with SAT-based methods.
Relevant literature: |
Research Project: Formal Methods in Computational Social Choice |
PI/Supervisor: Stefan Szeider
Show More 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: |
Research Project: SAT-Based 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: [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. [3] André Schidler, Stefan Szeider: SAT-based Decision Tree Learning for Large Data Sets. AAAI 2021: 3904-3912. |
Research Project: 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 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 Project: Proof Theory for Non-Classical 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 non-classical logics, and their exploitation. |
Research Project: Logic-based methods for AI Fairness |
PI/Supervisor: Agata Ciabattoni
Show More Algorithmic decision making may be inherently prone to unfairness, even when there is no intention for it. This is the case, for instance, when the data sets used with Machine Learning algorithms contain biases. In this project we explore the use of logical methods to tackle this issue. |
Research Project: Non-standard reasoning in Description Logic using solvers |
PI/Supervisor: Magdalena Ortiz co-Supervisor: Stefan Szeider Show More Description Logics (DLs) are a toolkit of decidable formalisms for representing knowledge, differing in their expressivity and in the computational cost of solving inference tasks. They are widely used in a range of application fields for writing “ontologies” that describe sharable domain knowledge. Efficient reasoners exist even for very expressive DLs in which reasoning has high computational complexity. However, there are many important reasoning services for which no practicable algorithms have been developed. This applies, specifically, to DL reasoning with numeric constraints on predicates, with different forms of data incompleteness, or with constraints on the size of models. These problems all have high worst-case computational complexity, and the few known techniques are not scalable beyond toy examples with a handful of predicates. The goal of this project is to develop scalable algorithms for this kind of reasoning services, particularly by exploiting efficient reasoners for combinatorial problems like SAT solvers, SMT solvers, QBF solvers, and (M)ILP solvers.A. Schidler, S. Szeider: SAT-based Decision Tree Learning for Large Data Sets. AAAI 2021: 3904-3912. C. Lutz, U. Sattler, L. Tendera: The complexity of finite model reasoning in description logics. Inf. Comput. 199(1-2): 132-171 (2005) |
Research Project: Ontology-based analysis of temporal data |
PI/Supervisor: Magdalena Ortiz co-Supervisor: Thomas Eiter Show More The Ontology-based data access (OBDA) paradigm facilitates access to data from possibly unstructured, incomplete, and disparate sources, by using an ontology as an intermediate layer that provides a unified view of the data described in a familiar high-level vocabulary. But despite its many successful applications, current OBDA technologies still have severe limitations that hinder their application in many more fields. In particular, the standard formalisms for accessing data are very poorly suited for analysing temporal and streaming data. In this project, we want to build on recently developed rule-based languages for temporal and streaming data (like LARS and DatalogMTL) to query and analyse data in OBDA systems. We want to tailor variants of these languages that can be paired with the ontology languages typically used in OBDA, to obtain rich declarative formalisms for temporal data analysis. The project is envisioned to cover both the theoretical study of the tailored formalisms, and practical challenges arising from real-life applications.S. Brandt, E. Güzel Kalayci, V. Ryzhikov, G. Xiao, and M. Zakharyaschev. Querying log data with metric temporal logic. J. Artif. Int. Res. 62, 1. 2018 https://doi.org/10.1613/jair.1 H. Beck, M. Dao-Tran, T. Eiter: LARS: A Logic-based framework for Analytic Reasoning over Streams. Artif. Intell. 261: 16-70 (2018). |
Research Project: Explainable reasoning with open- and closed-world knowledge bases |
PI/Supervisor: Magdalena Ortiz co-Supervisor: Thomas Eiter Show More In this project, we want to continue with the study of expressive Knowledge Representation languages that allow to combine open- and closed-world reasoning with rules and ontologies. We want to develop scalable algorithms for reasoning with knowledge bases in different fragments, and tailor variants that are better suited for real world use cases. We are also very interested in abductive automated reasoning techniques for explaining the inferences derived from such knowledge bases.L. Bajraktari, M. Ortiz, M. Simkus. Combining Rules and Ontologies into Clopen Knowledge Bases. AAAI 2018. S. Lukumbuzya, M. Ortiz, M. Simkus. Resilient logic programs: answer set programs challenged by ontologies. AAAI 2020. |
Research Project: Associative Web Search and Entity Set Expansion using Logical Reasoning |
PI/Supervisor: Georg Gottlob
Show More With associative web search, a user inputs a list of entities such as, for example, “BMW, Ford, Tesla” and obtains an expanded list with similar entities, in our example a list of all major car makes. The main technique for achieving associative web search is called entity set expansion (ESE). On a given input list, such as the one above, ESE makes web queries such as “+BMW +Ford +Tesla” using a standard search engine, and analyzes the first N (say N=100) results so as to discover lists in which the search entities co-occur with further entities. The original list is then expanded with these new entities. This expansion process is iteratively continued until hopefully all similar items (in our case, car makes) are found. ESE is, unfortunately, a rather error prone technique which has been improved using various statistical methods, as well as machine learning and clustering methods. The topic of this PhD project is to investigate knowledge-based and rule-based reasoning methods for improving ESE (possibly in combination with the formerly mentioned methods). This will involve the use of large general factual knowledge graphs such as Wikidata , Wordnet, and BabelNet, as well as specialized knowledge graphs and rule-bases for particular application domains. |
Research Project: 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. |
[/bg_collapse]
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.