VeriFIT Static Analysis Plugins

This page contains links to plugins developed by the VeriFIT group and implementing various static program analyses. More information about the plugins, including links to the repositories with their code as well as demo examples are available at the web pages of the particular plugins.

Logo VeriFIT Infer Plugins

L2D2: A Low-Level Deadlock Detector

L2D2 is a plugin of Facebook Infer for detecting low-level deadlocks in C/C++ programs. Development: Vladimir Marcin, Tomas Vojnar.

Atomer: Analysis of Atomicity of Sequences of Method Calls

Atomer is a plugin of Facebook Infer whose aim is (1) to detect sequences of method calls of C/C++ programs that are likely to execute atomically and (2) to detect cases where the atomicity is broken. Development: Dominik Harmim, Tomas Vojnar.

Looper: A Program Complexity Analyser

Looper is a plugin of Facebook Infer that is inspired by the Loopus analyser and whose aim is to automatically derive conservative complexity bounds. Development: Ondrej Pavela, Tomas Fiedor, Adam Rogalewicz, and Tomas Vojnar.