Direkt zum Inhalt | Direkt zur Navigation

Eingang zum Volltext

Lizenz

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:bsz:25-opus-73568
URL: http://www.freidok.uni-freiburg.de/volltexte/7356/


Malkis, Alexander

Cartesian abstraction and verification of multithreaded programs

Kartesische Abstraktion und Verifikation nebenläufiger Programme

Dokument1.pdf (649 KB) (md5sum: faa3a2b004d607a659fea1e78a4de1e2)

Kurzfassung in Englisch

A verification algorithm for concurrent programs that scales polynomially in the number of threads must be incomplete. For complete algorithms, all one can hope for is polynomial behavior on a practically interesting subclass. We give such an algorithm. The algorithm iteratively computes a counterexample-guided refinement of a known thread-modular verification method. The algorithm is provably polynomial on the practically interesting class of mutex programs. Our experiments show that it behaves well on mutex programs also in practice.


Kurzfassung in Deutsch

Ein Verifikationsalgorithmus für nebenläufige Programme, der in der Anzahl der Threads skaliert, ist zwangsläufig unvollständig. Für vollständige Algorithmen kann man höchstens ein polynomielles Verhalten auf einer praktisch interessanten Klasse erwarten. In dieser Arbeit geben wir einen solchen Algorithmus an. Der Algorithmus berechnet iterativ eine gegenbeispielgesteuerte Verfeinerung einer bekannten thread-modularen Methode. Der Algorithmus ist beweisbar polynomiell auf der Klasse der Programme mit Locks. Experimente zeigen, dass er mit der Klasse der Programme mit Locks auch in der Praxis gut auskommt.


SWD-Schlagwörter: Model Checking , Nebenläufigkeit , Abstrakte Interpretation , Verfeinerung , Verifikation , Korrektheit , Semantikerhaltende Transformation , Multithr
Freie Schlagwörter (deutsch): Abstrakte Interpretation , nebenläufige kartesische Abstraktion , gegenbeispielgesteuerte Abstraktionsverfeinerung
Freie Schlagwörter (englisch): abstract interpretation , multithreaded Cartesian abstraction , counterexample-guided abstraction refinement
CCS Klassifikation F.3.2 , F.3.1
Institut: Institut für Informatik
Fakultät: Technische Fakultät (bisher: Fak. f. Angew. Wiss.)
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Erstgutachter: Podelski, Andreas (Prof. Dr.)
Sprache: Englisch
Tag der mündlichen Prüfung: 10.02.2010
Erstellungsjahr: 2010
Publikationsdatum: 23.03.2010
Indexliste