Current 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...
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...
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...
Past projects
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...
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...