Research Projects

The Formal Methods in Systems Engineering Group at Vienna University of Technology is concerned with research and development in the following areas and projects:

APALACHE

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.

Website: forsyte.at/research/apalache/
Funding: Vienna Science and Technology Fund (WWTF)

Automated Program Analysis for Bounds on Resource Consumption

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.

Website: forsyte.at/research/resource-bound-analysis/
Funding: Vienna Science and Technology Fund (WWTF)

Heisenbugs: From Detection to Explanation

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.

Funding: Vienna Science and Technology Fund (WWTF)

LogiCS: Doctoral Program Logical Methods in Computer Science

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

Website: logic-cs.at/phd/
Funding: Austrian Science Fund (FWF)

RiSE: Rigorous systems engineering

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.

Website: arise.or.at/?id=nfn
Funding: Austrian Science Fund (FWF)

VCLA: Vienna Center for Logic and Algorithms


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.

Website: www.vcla.at
Funding: Vienna University of Technology

Former Projects

PROSEED: Proof Seeding for Software Verifications

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.

Further information
Funding: Vienna Science and Technology Fund (WWTF)

CANDI

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.

Website: www.candiproject.eu

Graduiertenkolleg PUMA (Programm- Und Modell-Analyse)
Doctorate Program PUMA (Program and Model Analysis)

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.

Website: puma.in.tum.de

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

Website: www.cased.de

FORTAS: FORmal Timing Analysis Suite

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

Website: fortastic.net
Funding: Austrian Science Fund (FWF) and German Research Foundation (DFG)

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.

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.

AIDA (EADS)

TAMORR (EADS)

 

Latest News

Helmut Veith 1971-2016

It is with the deepest sadness that we announce Helmut Veith’s passing on March 12, 2016. Helmut was a brilliant researcher, an inspiring collaborator, a stimulating teacher, a generous friend, and a wonderful father and husband. He leaves a void that will be impossible to fill. Our thoughts are with his family and friends.

Continue reading

Profil article on women in logic

A recent article in the Austrian weekly Profil about female logicians in Austria is featuring Agata Ciabattoni, Martina Seidl, Laura Kovacs, Magdalena Ortiz, Marijana Lazic, Shqiponja Ahmetaj, and Neha Lodha. All women are affiliated with the Doctoral College Logical Methods in Computer Science.  

Continue reading

Full news archive