Fluid Updates in Arbitrary Abstract Domains

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