Institute for Computer Languages
Compilers and Languages Group

CATPVS: Computer Algebra and Theorem Proving for Verified Software

Project details

Project summary

The objective of this project is to develop new methods of combining computer algebra and first-order theorem proving in static analysis of programs. We are going to develop new theory and algorithms for the automated synthesis of auxiliary program assertions that can be used to prove automatically the validity of safety and liveness properties of software.

Our project is structured on the following four research directions:


The following software tools are developed in the frame of our project:


The list of publications and talks based on the results of the project can be found here.

Contact: Laura Kovács.

Laura Kovács
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2015-02-20 (Webmaster)