1) Wider research context

Formal verification aims to ensure the correctness of complex systems, hardware designs,

and software. Unlike traditional testing methods, which rely on executing test cases, formal

verification analyses and validates system properties using precise mathematical

techniques and logical reasoning. The successful development of sophisticated automated

reasoning tools such as solvers for the boolean satisfiability (SAT) problem and computer algebra

algorithms opened up new perspectives and challenges for formal verification. Although both

SAT and computer algebra have a long history, they have only been utilized for problem solving

separately. Because of the absence of close integration, it is currently not possible to

simultaneously harness the strengths of both worlds for real-world problem solving in a single method.

2) Objectives

The mission of this project is to alter the reasoning landscape in bit-precise formal

verification by developing unique SAT-based algebraic methods for word-level reasoning over

polynomials. We focus on integrating SAT solving into algebraic reasoning over pseudo-boolean

integer polynomials, which are for instance used to verify hardware circuits, as well as

polynomials over finite domains, which can be used to model computer memory and cryptographic

encodings. We additionally develop proof logging techniques to certify the verification results.

3) Approach

The research in this project will follow two directions to achieve the goals:

(1) effective SAT solving for polynomial arithmetic, with a focus on (a) pseudo-boolean integer

polynomials, (b) finite fields, and (c) large words (i.e., bit-vectors); and (2) proof logging. We

extract state-of-the-art SAT paradigms and lift these techniques from propositional reasoning to

computer algebra by generalizing the identified inference algorithms to the selected polynomial

rings. Furthermore, we increase the capacity of algebraic proof calculi by incorporating proof

logging into all developed reasoning processes.

4) Level of innovation

Advancing formal method techniques is indispensable. Tightly linking algebraic reasoning with

SAT solving will enable us to fully exploit the potential of both techniques, and has the potential

to significantly increase the capacity of state-of-the-art methods for reasoning over finite fields,

large words, or pseudo-boolean integer polynomials. The timeliness of the proposed research

cannot be emphasized enough. Success in this project will yield unique theoretical and practical

solutions with practical applications in hardware verification, bit-vector reasoning, blockchain

technology and post-quantum cryptography, all of which are of high academic and industrial interest.

5) Primary researchers involved

Principal Investigator: Dr. Daniela Kaufmann (TU Wien)

Mentor: Prof. Laura Kovács (TU Wien)

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!

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.

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.

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, 

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.

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.

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. 

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.

Promt is a WWTF funded project, aiming to answer fundamental algorithmic questions related to verification of probabilistic programs. It is a joint project between IST Austria and the FORSYTE and TrustCPS groups from TU Wien. The project is split into three workpackages, each led by a principal investigator from one of the groups.

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.

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.

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.

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.

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).

The FORTAS project is concerned with execution time analysis of embedded software, focusing in particular on control software written in C.

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.

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.

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.

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.

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.

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.