Binary package “cbmc” in ubuntu jammy
bounded model checker for C and C++ programs
CBMC generates traces that demonstrate how an assertion can be violated, or
proves that the assertion cannot be violated within a given number of loop
iterations.