Computeralgebra und Theorembeweis fuer Softwareverifikation

01.04.2010 - 31.03.2013
Forschungsförderungsprojekt
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.

Personen

Projektleiter_in

Institut

Förderungsmittel

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

Forschungsschwerpunkte

  • Information and Communication Technology

Schlagwörter

DeutschEnglisch
Theorem BeweisTheorem Proving
InvariantInvariant Generation
Program VerifikationProgram Verification
OrdnungsfunktionenRanking Function