Institute for Computer Languages
Compilers and Languages Group
CATPVS: Computer Algebra and Theorem Proving for Verified Software
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:
- Assertion synthesis, where we focus on the automated generation of loop invariants and rankig functions;
- Automated program verification, where we combine assertion sythesis with verifiation condition generation;
- Proving program properties, where we develop new automated methods for first-order theorem proving;
- Tools and experiments, where we implement and evaluate our results.
The following software tools are developed in the frame of our project:
- ALIGATOR: software package for loop invariant generation;
- r-TuBound: software tool for the timing analysis of programs;
- Vampire: automated first-order theorem prover.
The list of publications and talks based on the results of the project can be found here.
Contact: Laura Kovács.
HTML 4.01 |
last update: 2015-02-20 (Webmaster)