Computeralgebra und Theorembeweis fuer Softwareverifikation

01.04.2010 - 31.03.2013
Research funding project
Das Ziel des vorliegenden Projektes ist es, neue kombinierte Methoden von Computeralgebra und Theorembeweisen erster Ordnung zur statischen Analyse von Programmen, zu erschliessen. Diese sollen bestehende Methoden der Softwareverifikation übertreffen, die nicht über derartige fortgeschrittene algebraische Techniken und deren Kombination mit Theorembeweisern erster Ordnung verfügen. Wir werden dabei neue Theorien und Algorithmen für die automatische Synthese von Auxiliary Program Assertations entwickeln, die automatisch die Gültigkeit der Safety- und Liveness- Eigenschaften von Software prüfen können.

People

Project leader

Institute

Förderungmittel

  • FWF - Österr. Wissenschaftsfonds (National) Fonds zur Förderung der wissenschaftlichen Forschung (FWF)

Research focus

  • Computational Intelligence: 100%

Keywords

GermanEnglish
Theorem BeweisTheorem Proving
InvariantInvariant Generation
Program VerifikationProgram Verification
OrdnungsfunktionenRanking Function

Publications