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:

Software

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

Publications

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

Contact: Laura Kovács.

Complang
Laura Kovács
   ARV
   ATCS
   Student-Projects
   Vinter
   Cade-Vampire-Tutorial
   SYNASC-Tutorial
   CATPVS
Sitemap
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2015-02-20 (Webmaster)