 Nie jesteś zalogowany | zaloguj się |
| Nie jesteś zalogowany | zaloguj się |
Prelegent: Tadeusz Sznuk
"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).
