Seminarium: Systemy Rozproszone
10 styczeń 2002, godzina 12:15, sala 3120
Piotr Kozieradzki P.Kozieradzki@students.mimuw.edu.pl


Metody wspomagające weryfikację kodu

Na seminarium chciałbym przedstawić dwa narzędzia opracowywane na uniwersytecie w Stanford, których zadaniem jest umożliwienie programiście zdefiniowanie pewnych warunków jakie jego zdaniem powinien spełniać kod aplikacji. Po zdefiniowaniu tych warunków istnieje możliwość sprawdzenia czy są one spełnione. Autorzy tych rozwiązań wprowadzili pewne założenia: takie narzędzie nie ma zawsze dawać dobrych odpowiedzi, pewnych warunków nie da się wyrazić a sprawdzanie odbywa się przede wszystkim na poziomie funkcji a nie globalnego przepływu wywołań w programie. Ich celem była efekywność, którą dokumentują przykładami z analizy tymi narzędziami kodu Linuxa, OpenBSD i protokołu FLASH.

Plan prezentacji

źródła

Strona domowa Pana Englera http://www.stanford.edu/~engler