Institute for Computer Languages
Compilers and Languages Group

CATPVS: Computer Algebra and Theorem Proving for Verified Software

---

Project details

• Project PI: Laura Kovács
• Funding agency: FWF - Austrian Science Fund
• Project number: T25-N23, Hertha Firnberg research grant
• Project period: April 1, 2010 - March 31, 2013

---

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:

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

Software

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.

Publications

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

Contact: Laura Kovács.