Fluid Updates in Arbitrary Abstract Domains

Prelegent(ci)

Tadeusz Sznuk

Afiliacja

Uniwersytet Warszawski

Termin

28 listopada 2011 10:15

Pokój

p. 4790

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

"Fluid updates" (płynne aktualizacje?) to mechanizm stosowany przy analizie programów operujących na tablicach, przedstawiony w pracy [DDA10]. Wykorzystuje on formuły logiki pierwszego rzędu, których spełnialność weryfikowana jest przez SMT-solver.

Podczas prezentacji pokażę, jak uogólnić ów mechanizm poprzez zastosowanie dowolnej dziedziny abstrakcyjnej zamiast FOL. Pozwoli to na wnioskowanie o dowolnych słownikach (niekoniecznie indeksowanych liczbami) oraz zwiększenie wydajności (poprzez zastąpienie wywołań SMT-solvera prostszymi operacjami np. na pentagonach).

---