smack


  • SMACK is a *bounded software verifier*, verifying the assertions in its input programs up to a given bound on loop iterations and recursion depth. SMACK can verify C programs, such as the following: