Detail výsledku

L2D2: A Low Level Deadlock Detector, Version 1.0

Vznik: 2020
Typ
software
Jazyk
anglicky
Autoři
Marcin Vladimír, Ing., FIT (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Popis

L2D2 version 1.0 is the first version of a static detector of deadlocks in concurrent programs written in C, C++, or Java and using low-level synchronisation by explicit mutex locking and unlocking. The tool is a static analyser based on abstract interpretation and function summaries, which are computed along the call tree, starting from its leaves so as to achieve good scalability. The detector is implemented in Ocaml as a plugin of the Facebook Infer Framework.

Klíčová slova

Concurrent programs, multithreaded programs, low-level synchronisation, mutexes, deadlocks, static analysis, abstract interpretation, function summaries, Facebook Infer.

URL
Licence
K využití výsledku jiným subjektem je vždy nutné nabytí licence
Licenční poplatek
Poskytovatel licence na výsledek nepožaduje licenční poplatek
Licenční podmínky

Volně šiřitelný software poskytovaný pod MIT licencí (přesné znění licence je dostupné na stránce https://opensource.org/licenses/MIT).

Projekty
AQUAS: Agregované metody řízení kvality, EU, Horizon 2020, 8A17001, 737475, zahájení: 2017-05-01, ukončení: 2020-04-30, ukončen
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru