An effective bug finder for C

Download .zip Download .tar.gz

EBA is a prototype tool to find non-trivial resource manipulation bugs in C programs, at compile-time, and super-fast.

In its few months of existence, EBA has found several double-lock bugs in Linux 4.7–4.10 releases (i.e. in code that has passed code reviews). All the following bugs are caught by EBA in a matter of seconds:

[1] I reported this bug in private email communication with Kalle Valo, but I was slow and the bug had been found and fixed already.

[2] I was slow at reporting this bug too.

[3] For some reason I was not credited, but I reported this bug! Sometimes I reported publicly and sometimes privately by emailing the maintainers.

[4] To be confirmed.


EBA is open source: https://github.com/iagoabal/eba

(There are installation instructions in the README.md file.)


EBA first uses side-effect analysis to build a program abstraction. This abstraction is later model checked in search of bug patterns.


EBA is a tool by Iago Abal.

This project was originally part of my PhD at IT University of Copenhagen, where I worked together with Andrzej Wąsowski and Claus Brabrand.