Bitte warten...
Bitte warten...
English
Hilfe
Login
Forschungsportal
Suche
Forschungsprofile
Forschungsprojekte
Projektvollmacht
Lehre
Forschung
Organisation
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
Univ.Prof.in Dr.in techn. Laura Kovacs MSc
(E185)
Institut
E185 - Institut für Computersprachen
Förderungsmittel
FWF - Österr. Wissenschaftsfonds (National)
Forschungsschwerpunkte
Information and Communication Technology
Schlagwörter
Deutsch
Englisch
Theorem Beweis
Theorem Proving
Invariant
Invariant Generation
Program Verifikation
Program Verification
Ordnungsfunktionen
Ranking Function