VeriFIT Static Analysis Plugins

This page contains links to plugins developed by the VeriFIT group (currently for Meta/Facebook Infer and Frama-C) that implement 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.

L2D2: A Low-Level Deadlock Detector

L2D2 is a plugin of Meta/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 Meta/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 Meta/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.

Deadlock: Deadlock Detection in Frama-C

Deadlock is a plugin of Frama-C that is inspired by the Racer-X analyser and whose aim is to search for potential deadlocks in C code. Unlike L2D2, Deadlock uses a classical forward anylysis. Development: Tomas Dacik and Tomas Vojnar.