EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs (Competition Contribution)

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

23 Downloads (Pure)


Combining different verification and testing techniques together could, at least in theory, achieve better results than each individual one on its own. The
challenge in doing so is how to take advantage of the strengths of each technique while compensating for their weaknesses. EBF 4.2 addresses this challenge for concurrency vulnerabilities by creating Ensembles of Bounded model checkers and gray-box Fuzzers. In contrast with portfolios, which simply run all possible techniques in parallel, EBF strives to obtain closer cooperation between them. This goal is achieved in a black-box fashion. On the one hand, the model checkers are forced to provide seeds to the fuzzers by injecting additional vulnerabilities in the program under test. On the other hand, off-the-shelf fuzzers are forced to explore different interleavings by adding lightweight instrumentation and systematically re-seeding them.
Original languageEnglish
Title of host publication29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
Publication statusAccepted/In press - 11 Feb 2023


Dive into the research topics of 'EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs (Competition Contribution)'. Together they form a unique fingerprint.

Cite this