Result Details

L2D2: A Low Level Deadlock Detector, Version 1.0

Created: 2020
Type
software
Language
English
Authors
Marcin Vladimír, Ing.
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Description

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.

Keywords

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

URL
License
In order to use the result by another entity, it is always necessary to acquire a license
License Fee
The licensor does not require a license fee for the result
License Conditions

Free software under the MIT license (cf. https://opensource.org/licenses/MIT).

Projects
AQUAS: Aggregated Quality Assurance for Systems, EU, Horizon 2020, 8A17001, 737475, start: 2017-05-01, end: 2020-04-30, completed
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top