Computer Algebra abd Theorem Proving for Verified Software

01.04.2010 - 31.03.2013
Research funding project
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.

People

Project leader

Institute

Grant funds

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

Research focus

  • Computational Intelligence: 100%

Keywords

GermanEnglish
Theorem BeweisTheorem Proving
InvariantInvariant Generation
Program VerifikationProgram Verification
OrdnungsfunktionenRanking Function

Publications