The four pillars of FORSYTE are:
- Automated Program Reasoning (Kovács)
- Theory and Applications of Satisfiability (Fazekas)
- Models Of Computation (Zuleger)
- Rigorous Systems Engineering (Weissenbacher)
The research unit is concerned with the development of both theoretical foundations and practical approaches for software and hardware verification and engineering.
Fundamental research topics include software model checking, test case generation, static analysis, protocol verification, and formal methods for distributed and concurrent systems. Industrial research is focusing on low level software, and embedded systems in the avionics and automotive sector.
CalgSAT: Combining Computer Algebra with SAT for Word-Level Reasoning
Begin/end: 2024-06-01 - 2027-05-31
Description: <p>1) Wider research context</p> <p>Formal verification aims to ensure the correctness of complex systems, hardware designs,</p> <p>and software. Unlike traditional testing methods, which rely on executing test cases, formal</p> <p>verification analyses and validates system properties using precise mathematical</p> <p>techniques and logical reasoning. The successful development of sophisticated automated</p> <p>reasoning tools such as solvers for the boolean satisfiability (SAT) problem and computer algebra</p> <p>algorithms opened up new perspectives and challenges for formal verification. Although both</p> <p>SAT and computer algebra have a long history, they have only been utilized for problem solving</p> <p>separately. Because of the absence of close integration, it is currently not possible to</p> <p>simultaneously harness the strengths of both worlds for real-world problem solving in a single method.</p> <p>2) Objectives</p> <p>The mission of this project is to alter the reasoning landscape in bit-precise formal</p> <p>verification by developing unique SAT-based algebraic methods for word-level reasoning over</p> <p>polynomials. We focus on integrating SAT solving into algebraic reasoning over pseudo-boolean</p> <p>integer polynomials, which are for instance used to verify hardware circuits, as well as</p> <p>polynomials over finite domains, which can be used to model computer memory and cryptographic</p> <p>encodings. We additionally develop proof logging techniques to certify the verification results.</p> <p>3) Approach</p> <p>The research in this project will follow two directions to achieve the goals:</p> <p>(1) effective SAT solving for polynomial arithmetic, with a focus on (a) pseudo-boolean integer</p> <p>polynomials, (b) finite fields, and (c) large words (i.e., bit-vectors); and (2) proof logging. We</p> <p>extract state-of-the-art SAT paradigms and lift these techniques from propositional reasoning to</p> <p>computer algebra by generalizing the identified inference algorithms to the selected polynomial</p> <p>rings. Furthermore, we increase the capacity of algebraic proof calculi by incorporating proof</p> <p>logging into all developed reasoning processes.</p> <p>4) Level of innovation</p> <p>Advancing formal method techniques is indispensable. Tightly linking algebraic reasoning with</p> <p>SAT solving will enable us to fully exploit the potential of both techniques, and has the potential</p> <p>to significantly increase the capacity of state-of-the-art methods for reasoning over finite fields,</p> <p>large words, or pseudo-boolean integer polynomials. The timeliness of the proposed research</p> <p>cannot be emphasized enough. Success in this project will yield unique theoretical and practical</p> <p>solutions with practical applications in hardware verification, bit-vector reasoning, blockchain</p> <p>technology and post-quantum cryptography, all of which are of high academic and industrial interest.</p> <p>5) Primary researchers involved</p> <p>Principal Investigator: Dr. Daniela Kaufmann (TU Wien)</p> <p>Mentor: Prof. Laura Kovács (TU Wien)</p>AbInfVS:
Begin/end: 2023-04-03 - 2025-12-31
Description: <p>In der heutigen digitalen Welt ist Informatik zu einem Thema geworden, das jede*n betrifft. Mit unserem Projekt setzen wir unsere Überzeugung in die Tat um, dass der beste Weg Informatik zu verstehen, ist, ihre Grundprinzipien selbst auszuprobieren –je früher, desto besser!</p> <p>Unser Projekt organisiert deshalb Workshops um Volksschulkindern lebensnahe Themen der Informatik zu vermitteln. Es geht nicht ums Programmieren, sondern die Kinder lösen 2-3 Aufgaben mittels logischem Denken und zwar "unplugged", ohne Computer. Durch das Lösen erleben die Kinder in vielen AHA-Momenten was Informatik ist.</p>CGC: CGC - Changing Gendered Cultures
Begin/end: 2024-10-01 - 2026-09-30
Description: <p>TU Wien has been striving for a holistic approach to equal opportunities for years. We believe that the recruitment of female students and scientists and their career development are interrelated issues. The proposed project is therefore a mix of measures that will help us to continue our gender policy in a proven manner. One focus is on working with primary school girls to make computer science a conceivable career choice at a very early stage. The other activities are aimed at the retention and career development of women by promoting the zero-tolerance approach to gender-based violence. All members of TU Wien have a claim and a right to the protection of their personal integrity. Beyond the legal obligation to protect against sexual harassment, TU Wien takes a clear stance against any kind of harassing, transgressive behavior. This includes also to take very specific measures to change the culture at the faculty with the lowest proportion of women. </p>ARTIST: Automated Reasoning with Theories and Induction for Software Technologies
Begin/end: 2021-07-01 - 2026-06-30
Description: <p>The long list of software failures over the past years calls for serious concerns in our digital society, creating bad reputation and adding huge economic burden on organizations, industries and governments. Improving software reliability is no more enough, ensuring software reliability is mandatory. Our project complements other advances in the area and addresses this demand by turning first-order theorem proving into an alternative, yet powerful approach to ensuring software reliability, </p> <p><br></p> <p>Saturation-based proof search is the leading technology for automated first-order theorem proving. The high-gain/high-risk aspect of our project comes from the development and use of saturation-based theorem proving as a unifying framework to reason about software technologies. We use first-order theorem proving methods not only to prove, but also to generate software properties that imply the absence of program errors at intermediate program steps.</p> <p><br></p> <p>Generating and proving program properties call for new methods supporting reasoning with both theories and quantifiers. Our project extends saturation-based first-order theorem provers with domain-specific inference rules to keep reasoning efficient. This includes commonly used theories in software development, such as the theories of integers, arrays and inductively defined data types, and automation of induction within saturation-based theorem proving, contributing to the ultimate goal of generating and proving inductive software properties, such as invariants.</p> <p><br></p> <p>Thanks to the full automation of our project, our results can be integrated and used in other frameworks, to allow end-users and developers of software technologies to gain from theorem proving without the need of becoming experts of it. </p>
APALACHE
Website: http://forsyte.at/research/apalache/
Funding: Vienna Science and Technology Fund (WWTF)
Critical distributed systems are designed to tolerate faults of individual components: they must work even if some of their components fail. In APALACHE, we address two technical and methodological challenges: Domain-specific abstraction for fault-tolerant TLA+ designs, and parameterized model checking techniques for an unbounded number of components.
Heisenbugs: From Detection to Explanation
Funding: Vienna Science and Technology Fund (WWTF)
Heisenbugs are software bugs that defy attempts to analyse their causes. The project, funded by a WWTF Vienna Research Groups for Young Investigators grant, is concerned with the detection, reproduction, and explanation of intricate error scenarios in concurrent programs and embedded systems.
LogiCS: Doctoral Program "Logical Methods" in Computer Science
Website: http://logic-cs.at/phd/
Funding: Austrian Science Fund (FWF)
The LogiCS doctoral program is a PhD degree program funded by the Austrian Science Fund FWF and run jointly by the three Austrian universities Vienna University of Technology, Graz University of Technology and Johannes Kepler University Linz.
Automated Program Analysis for Bounds on Resource Consumption
Website: http://forsyte.at/research/resource-bound-analysis/
Funding: Vienna Science and Technology Fund (WWTF)
Computer programs are consuming physical resources such as time, memory, power and bandwidth. To guarantee that a program only uses a limited amount of these resources, programmers need automated tools which predict the resource consumption of a program. In this project, we will develop such methods and tools for resource prediction.
RiSE: Rigorous systems engineering
Website: http://arise.or.at/?id=nfn
Funding: Austrian Science Fund (FWF)
The National Research Network “RiSE: Rigorous systems engineering” is funded by the Austrian Science Fund (FWF). RiSE investigates techniques beyond classical model checking and a-posteriori verification.
VCLA: Vienna Center for Logic and Algorithms
Website: http://www.vcla.at/
Funding: Vienna University of Technology
The Vienna Center for Logic and Algorithms (VCLA) is an initiative of Vienna University of Technology (TU Vienna). Located at the Faculty of Informatics, the Center is promoting international scientific collaboration in logic and algorithms.
Former Projects
AIDA (EADS)
BASE.XT (BMW)
Within the BASE.XT project a rigorous model-driven development (MDD) approach for software-intensive automotive systems has been developed in cooperation with BMW Group. The COLA-IDE, i.e., the authoring tool supporting this MDD approach, facilitates modelling on different levels of abstraction (requirements specification and analysis, behavioral modelling, and modelling of the execution platform) aiming at complexity reduction and separation of concerns. Several case studies demonstrated the feasibility of the presented approach.
CANDI
Website: http://www.candiproject.eu/
The CANDI project will develop both the infrastructure for e-Learning / Retraining, and the skills necessary to transfer existing courses and curricula to an e-Learning environment.
CASED
Website: https://www.cysec.tu-darmstadt.de/en/research/collaborative-projects/cased/
The Center for Advanced Security Research Darmstadt (CASED) is headquarter to a cluster of computer scientists, engineers, physicist, legal experts and experts in business administration located at TU Darmstadt, Fraunhofer SIT and Hochschule Darmstadt (University of Applied Sciences).
FORTAS: FORmal Timing Analysis Suite
Website: http://fortastic.net/
Funding: Austrian Science Fund (FWF), German Research Foundation (DFG)
The FORTAS project is concerned with execution time analysis of embedded software, focusing in particular on control software written in C.
InteCo
The InteCo (Intelligent Cockpit) project investigates the integration of formal methods into the development processes of airborne software systems. In this project we developed a novel approach to combine model-based testing with systematic test input generation for C code in order to determine deviations of requirements and implementation automatically.
PROSEED: Proof Seeding for Software Verifications
Website: https://wwtf.at/programmes/information_communication/ICT10-050
Funding: Vienna Science and Technology Fund (WWTF)
The PROSEED research project proposes an innovative approach to verification which is based on the insight that program texts are carrying important information which is directed at the human readers of the program. We will utilize this human engineering information in a logically sound framework for computer-aided verification.
Graduiertenkolleg PUMA (Programm- Und Modell-Analyse) Doctorate Program PUMA (Program and Model Analysis)
Website: http://puma.in.tum.de/
The doctorate program (Graduiertenkolleg) PUMA brings together the four fundamental approaches of program and model analysis, namely, type systems, theorem proving, model-checking, and abstract interpretation. Its goal is to develop new analysis techniques through cross-fertilization. The new methods should prototypically be implemented and be evaluated on selected analysis problems of software-intensive systems.
TAMORR (EADS)