Fluid Updates in Arbitrary Abstract Domains

Speaker(s)

Tadeusz Sznuk

Affiliation

Uniwersytet Warszawski

Date

Nov. 28, 2011, 10:15 a.m.

Room

room 4790

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

"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).

---