Computer Algebra abd Theorem Proving for Verified Software

01.04.2010 - 31.03.2013
Forschungsförderungsprojekt
The objective of the project is to develop new methods of combining computer algebra and first-order theorem proving in static analysis of programs. This will enable verification of programs that are beyond the power of existing methods since advanced computer algebra techniques and their combination with first-order theorem proving are not used in state-of-the-arts verification tools. 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.

Personen

Projektleiter_in

Institut

Grant funds

  • FWF - Österr. Wissenschaftsfonds (National) Austrian Science Fund (FWF)

Forschungsschwerpunkte

  • Computational Intelligence: 100%

Schlagwörter

DeutschEnglisch
Theorem BeweisTheorem Proving
InvariantInvariant Generation
Program VerifikationProgram Verification
OrdnungsfunktionenRanking Function

Publikationen