Current Projects
Research Projects at the Institute
EU-funded Projects
LogiCS@TUWien (Doctoral Programme)
Funding: EU-H2020 Marie Skłodowska-Curie COFUND
Time Frame: started 01. 06. 2022
Contact Persons: Ezio Bartocci
Research Team: Ezio Bartocci (vice-chair for admission program), Stefan Szeider (chair), Thomas Eiter, Magdalena Ortiz (vice-chair for publicity and outreach), Stefan Woltran, Robert Ganian, Agata Ciabattoni (vice-chair for ethics), Pavol Cerny, Georg Gottlob, Georg Weissenbacher, Matteo Maffei, Laura Kovacs, Florian Zuleger (vice-chair for research and training)
LogiCS@TUWien is an interdisciplinary Marie Skłodowska-Curie COFUND doctoral programme at Technische Universität Wien (TU Wien) that educates 20 PhD students for 4 years on logical methods in Computer Science and their applications, in particular to Artificial Intelligence, Databases, Verification, Algorithms, Security and Cyber-Physical Systems.
AT-funded Projects
CPS/IoT Ecosystem: Preparing Austria for the Next Digital Revolution
Funding: AT-BMWFW: HRSM Grant
Partners: TU Wien, Austrian Institut of Technology (AIT), Institute of Science and Technology (IST)
Time Frame: started 01. 06. 2017
Research Team: Manfred Gruber (AIT), Thomas A. Henzinger (IST), Schahram Dustdar, Dejan Nickovic (AIT), Gerti Kappel
Cyber-physical systems (CPS) are spatially-distributed, time-sensitive, multiscale networked embedded systems, connecting the physical world to the cyber world through sensors and actuators. The Internet of Things (IoT) is the backbone of CPS. It connects the Sensors and Actuators to the nearby Gateways and the Gateways to the Fog and the Cloud. The Fog resembles the human spine, providing fast and adequate response to imminent situations. The Cloud resembles the human brain, providing large storage and analytic capabilities.
In this project we will make Austria a major player in Real-Time (RT) CPS/IoT, by building on its national strengths. In collaboration with renowned Austrian companies such as TTTech or ams AG, we will create an RT CPS/IoT-Ecosystem with more than 5000 sensors and actuators, where we can all experiment with new ideas, and develop this way an Austrian know-how. This effort will be aligned with the strategic Austrian initiatives, Industry 4.0 and Silicon-Austria. The ecosystem will be distributed across Vienna in collaboration with our partners at AIT and IST.
Digital Modeling of Asynchronous Integrated Circuits
Funding: Austrian Science Fund (FWF)
Collaborators: Matthias Függer (ENS Paris-Saclay),Thomas Nowak (Université Paris-Sud), Sayan Mitra (U. Illinois at Urbana-Champaign), Laura Nenzi (U. of Trieste), Ezio Bartocci (TU Wien)
Time Frame: started 01. 07. 2019
Contact Persons: Ulrich Schmid
Research Team: Ulrich Schmid
The project Digital Modeling of Asynchronous Integrated Circuits (DMAC) is devoted to the development of a purely digital model for asynchronous circuits, which enables accurate and fast dynamic timing analysis and is a mandatory prerequisite for any attempt on practical formal verification of such designs. The envisioned model shall be accurate and realistic (= faithful), in the sense that the behavior of circuits described in the model is exactly, i.e., within the modeling accuracy, the same as the behavior of the corresponding real circuit. In contrast to analog models, which are known to be faithful but suffer from excessive simulation times, we target continuous-time discrete-value models here, which essentially boil down to elaborate delay models for gates and/or interconnecting channels.
The project builds on our novel involution model, which considers input-to-output delays as as function of the history in the signal trace. DMAC will fully explore this avenue scientifically, by answering questions such as how to enlarge the class of circuits where the involution model and variants thereof are faithful, how to compose gates with different electrical properties, in particular, different threshold voltage levels, how to accurately model subtle delay variation originating in the Charlie effect in multi-input gates, how to parametrize and characterize the model for a given technology and given operating conditions, and how to possibly further improve the modeling coverage and accuracy. In addition, we will also make the first steps to incorporate our models into existing timing analysis and verification tools for validation purposes.
ProbInG: Distribution Recovery for Invariant Generation of Probabilistic Programs
Funding: AT-WWTF
Partners: TU Wien
Time Frame: started 01. 05. 2020
Contact Persons: Ezio Bartocci
Research Team: Ezio Bartocci, Efstathia Bura (co-PI), Laura Kovacs (co-PI)
Probabilistic programming is a new emerging paradigm adopted by high-tech giants, such as Google, Amazon and Uber, to simplify the development of AI/machine learning based applications, such as route planning and detecting cyber intrusions.
Probabilistic programming languages include native constructs for sampling distributions allowing to freely mix deterministic and stochastic elements. The resulting flexible framework comes at the price of programs with behaviors hard to analyze, leading to unpredictable adverse consequences in safety-critical applications.
One of the main challenges in the analysis of these programs is to compute invariant properties that summarize loop behaviors. Despite recent results, full automation of invariant generation is at its infancy and only targets expected values of the program variables, which is insufficient to recover the full probabilistic program behavior.
Our project aims at developing novel and fully automated approaches to generate invariants over higher-order moments and the value distribution of program variables, without any user guidance. We will employ methods from symbolic summation, polynomial algebra and statistics and combine them with static analysis techniques.
Our results will reduce the need of expert knowledge in ensuring the safety and security of computer systems and will cut the design costs of applications based on probabilistic programs, bringing crucial intellectual and economic benefits to our society.
Reasoning about Knowledge in Byzantine Distributed Systems
Funding: Austrian Science Fund (FWF)
Time Frame: started 01. 07. 2020
Contact Persons: Roman Kuznets, Ulrich Schmid
Research Team: Roman Kuznets, Ulrich Schmid, Giorgio Cignarale, Krisztina Fruzsa, Rojo Fanamperana Randrianomentsoa, Hugo Rincon Galeana, Thomas Schlögl
Reasoning about fault-tolerant distributed systems, which consist of networked processors without a central control that need to achieve a common goal, is notoriously difficult due to the many sources of uncertainty: varying execution speeds, unpredictable transmission delays, and partial failures make it difficult for a processor to establish local knowledge sufficient to safely perform required actions.
The goal of the proposed project is to incorporate arbitrarily misbehaving agents into an epistemic reasoning framework and to supplement the standard Kripke semantics with a suitable topological semantics for distributed systems, while exploiting, and being informed by, the success of Dynamic Epistemic Logic in capturing the dynamics of knowledge evolution in modal logic.
SecInt - Secure and Intelligent Human-Centric Digital Technologies (Doctoral College)
Funding: AT-TU Wien
Partners: TU Wien
Time Frame: started 01. 09. 2020
Contact Persons: Ezio Bartocci, Tanja Zseby, Matteo Maffei
Research Team: Ezio Bartocci, Tanja Zseby (co-speaker), Thomas Gärtner, Martina Lindorfer, Andreas Kugi, Georg Weissenbacher, Semeen Rehman, Laura Kovacs, Efstathia Bura, Matteo Maffei (speaker)
Digitalization is transforming our society, making our everyday life more and more dependent on computing platforms and online services. These are built so as to sense and process the environment in which we live as well as the activities we carry on, with the ultimate goal of returning predictions and taking actions to support and enhance our life. Prominent examples of this trend are autonomous systems (e.g., self-driving cars and robots), cyber-physical systems (e.g., implanted medical devices), apps in wearable devices (e.g., Coronavirus contact tracing apps), and so on. Despite the interest of stakeholders and the attention of the media, digital technologies that so intimately affect human life are not yet ready for widespread deployment, as key technical and ethical questions are open, such as trustworthiness, security, and privacy. If these problems are not solved, supposedly intelligent human-centric technologies can lead to death or to other undesirable consequences: e.g., the learning algorithms of autonomous cars can be fooled so as to cause crash accidents, implanted medical devices can be remotely hacked to trigger unwanted defibrillations, and contact tracing apps can be misused towards an Orwellian surveillance system or to inject false at-risk alerts.
The goal of SecInt is to develop the scientific foundations of secure and intelligent human-centric digital technologies. This requires interdisciplinary research, establishing synergies in different research fields (Security and Privacy, Machine Learning, and Formal Methods). Research highlights brought forward by the synergies across projects include the design of machine learning algorithms resistant to adversarial attacks, the design of machine learning algorithms for security and privacy analysis, the security analysis of personal medical devices, the design of secure and privacy-preserving contact tracing apps, and the enforcement of safety for dynamic robots.
The research development is accompanied by a supporting educational and training programme, which encompasses the ethics of secure and intelligent digital technologies, interdisciplinary technical knowledge, as well as internships in international elite research partners, which expressed interest to collaborate with SecInt.