Current Projects
AIDE
To help software developers to cope with the huge and ever-increasing complexity of software, the project aims at new techniques of automated analysis and verification of advanced software, which uses low-level programming, new high-level constructs, or both. To obtain such methods, the project intends to build primarily on various logic-based approaches, such as bi-abductive analysis or symbolic execution, suitably combined with methods like abstract interpretation, slicing, and advanced type systems. To increase the efficiency of the considered logic-based methods, the project will also develop or significantly improve decision procedures for the various considered logics (e.g., separation logic, quantified bit-vector logic, or constrained Horn clauses). The low-level programs to be verified include especially programs with low-level pointer manipulation and dynamic-linked data structures, while the considered high-level programs include programs based on expert systems, high-level specifications of software, and programs in modern high-level languages like Scala. More...
ExtremeXP: EXPerimentation driven and user eXPerience oriented analytics for eXtremely Precise outcomes and decisions
Extreme data characteristics (volume, speed, heterogeneity, distribution, diverse quality, etc.) challenge the state-of-the-art data- driven analytics and decision-making approaches in many critical domains such as crisis management, predictive maintenance, mobility, public safety, and cyber-security. At the same time, data-driven insights need to be extremely timely, accurate, precise, fit- for-purpose, and trustworthy, so that they can be useful. ExtremeXP will handle the complexity of matching extreme needs with complex analytics processes (i.e., processes that involve and combine ML, data analysis, simulation and visualization components) by placing the end user at the centre of complex analytics processes and relying on user intents and running experiments (i.e., trial and error) to prune the vast solution space of possible analytics workflows and configurations i.e., “variants”. Its main goal is to create a next generation decision support system that integrates novel research results from the domains of data integration, machine learning, visual analytics, explainable AI, decentralised trust, knowledge engineering, and model-driven engineering into a common framework. The overarching idea of the framework is to optimise the properties of a complex analytics process that the end user cares about (e.g., accuracy, time-to-answer, specificity, recall, precision, resource consumption) by associating user profiles to computation variants. The framework is envisioned as modular and extensible, orchestrating different services around an Experimentation Engine: Analysis-aware Data Integration, Extreme Data & Knowledge Management, User-driven AutoML, Transparent & Interactive Decision Making, and User-driven Optimization of Complex Analytics. The framework will be validated in five pilot demonstrators. More...
Type systems for data-centric programming
Static type systems are a popular and effective tool for writing robust and correct programs. They are used to check how programs access memory, call sub-components and communicate over the network. Unfortunately, conventional static type systems are inadequate for checking properties of programs that transform, explore and visualise data. Such programs use a terse, flexible and highly dynamic programming style whose subtle logic are not readily tracked using standard notions of types, making data-centric programming difficult and error-prone. This project will develop new foundational type system concepts for data-centric programming in languages such as R and Python. We will initially focus on two specific application areas (data frames and the grammar of graphics) where a small change in parameters often has wide-ranging implications on the program logic. We will develop a family of novel type systems, describe them formally and prove their safety. The design will leverage recent techniques (some developed by the PI) including coeffects, type providers, graded types and refinement types and it will be informed by an empirical analysis of large open-source code repositories. More...
Past Projects
AFarCloud: Aggregate Farming in the Cloud
AFarCloud addresses the urgent need for a holistic and systematic approach. It will provide a distributed platform for autonomous farming, which will allow the integration and cooperation of Cyber Physical Systems in real-time for increased agriculture efficiency, productivity, animal health, food quality and reduced farm labour costs. This platform will be integrated with farm management software and will support monitoring and decision-making, based on big data and real time data mining techniques. More...
ASCENS: Autonomic service-component ensembles
Self-aware, self-adaptive and self-expressive autonomic components, running within environments which are called “ensembles”, have been proposed to handle open-ended, highly parallel, massively distributed systems that can span millions of nodes with complex interactions and behaviors. More...
Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures
This project targets the area of automated verification of computer systems, which currently attracts a lot of attention both in academia as well as industry. The reasons are clear: The complexity of computer systems is constantly growing, and it is more and more difficult to ensure their correct functionality. At the same time, many fully automated computer systems are used in increasingly critical applications (such as control of industrial plants, cars, planes, space devices, etc.). Moreover, expectations of users to be provided with reliable products are growing even for common everyday applications (e.g., office software or various home electronics that is nowadays usually computer-controlled). More...
ESTABLISH
The aim of ESTABLISH is to convert (sensor) data into actionable information developing software intense applications that combine real time sensor data with models providing real time feedback. The application scope is services and solutions on an individual level utilizing environmental sensors (air quality, noise, heat, temperature) to improve our quality of life with respect to health. More...
FitOptiVis: From the cloud to the edge
FitOptiVis will balance power demand versus performance of the increasingly complex distributed configurations in Cyber-Physical Systems, reflected in the growing number of sensors, actuators and other smart devices, their growing autonomy, and the increased need for performance. This complexity increases even more when multiple heterogeneous sensor inputs are combined for analysis and through integration of both generic and specialised devices. On top of that, CPS need to satisfy rigorous constraints on real-time behaviour, safety, security, reliability, quality, performance and energy consumption. FitOptiVis will provide end-to-end multi-objective optimisation for imaging and video pipelines of CPS, with an emphasis on the latter two elements – energy and performance. More...
FluidTrust
The significant increase in the ubiquity and connectivity of computing devices has opened new possibilities for addressing social, environmental and other challenges in multiple domains. One of domains is Industry 4.0 where systems are subject to multiple specifics: they are highly dynamic and open-ended and most importantly they are plagued with uncertainty - i.e. they have to deal with unforeseen changes in their environment, limited connectivity, emergency situations, etc. These two characteristics emerge in all aspects of these systems. From these however, the aspect of trust, which comprises the security and privacy, starts to stand out as one of the most important aspects for wide adoption of Industry 4.0. The vision of the project is to address the novel combination of high level of uncertainty and high level of dynamicity and aim at providing formal models and analysis methods for specification, runtime enforcement and guarantees of access control in highly dynamic and uncertain systems of the Industry 4.0 domain. More...
ROBUST
Automated software verification and bug hunting are a hot topic in both industry and academia. Indeed, they can save a lot of money and, in case of safety-critical software, even human lives. This project aims at new automated methods of static formal verification (based on approaches like symbolic verification or automated abstraction) as well as extrapolating dynamic analysis and advanced testing of programs that use several classes of advanced programming constructions. More...
SNAPPY
Due to the complexity of current software and the rising requirements on its reliability, traditional testing no longer suffices to assure the needed quality, and automated analysis and verification methods are needed. However, despite a lot of recent progress in this area, the current methods are still lacking in scalability, precision, and/or capabilities of analysing complex properties of advanced code. The goal of the project is to significantly improve state-of-the-art techniques of automated analysis and verification to make them more scalable and applicable for handling more complex properties of more complex code with low-level pointer operations, arrays, strings, and/or concurrency. More...
TRUST 4.0
TRUST 4.0 project aims at ensuring privacy and trust in ad-hoc cooperation within and across organizations in a supply chain in an Industry 4.0 environment. The project targets several objectives, e.g., enforcing trust in the dynamic Industry 4.0, facilitating trust provision by improving trust analyses and techniques etc. More...