model-checking

7Ciepło

1Odpowiedz

Trafność sprawdzania modelu w mocno typowanych językach programowania funkcjonalnego?

Obecnie uczę się sprawdzać model (logika modalna, LTL, CTL, sprawdzanie modelu SAL, itp.) Iw wolnym czasie uczę się o Idrisie, który jest silnie typowanym językiem programowania funkcjonalnego, który

idris model-checking 2016-04-07

---

5Ciepło

1Odpowiedz

Omijanie niepodpisane dodawania przepełnienia wykryte przez CBMC

CBMC wykrywa ewentualne przepełnienie unsigned dodawanie w następujących liniach: l = (t + *b)&(0xffffffffL); c += (l < t); Zgadzam się, że istnieje możliwość przepełnienia w pierwszej linii, ale j

c integer integer-overflow model-checking cbmc 2015-06-26

---

5Ciepło

1Odpowiedz

Sprawdzanie modelu LTL za pomocą składni Spin i Promeli

Próbuję odtworzyć kod ALGOL 60 napisany przez Dijkstra w artykule zatytułowanym "Współpracujące procesy sekwencyjne", kod jest pierwszą próbą rozwiązania problemu z muteksem, tutaj jest składnia: begi

model-checking spin promela 2013-03-05

---