I was one of the students accepted in the SSRF Program in the summer of 2023. I worked in the Programming Methodology group under supervision of Dr. Peter Muller, and Dr. Marco Eilers.
My main task during this internship was to find a way to integrate CBMC into Viper, as a bounded model checker. In many cases, fully verifying a program might not be efficient or even possible, so the main idea here was to use model checking as a remedy to this problem. First step was to find a way to model Viper language in C, and then to see if CBMC is the right tool. We modeled some of the features including inhale, exhale, predicate, etc.
CBMC had one main issue with universal quantifiers, where it would simply ignore them in many cases, resulting in a false result. We needed quantifiers to model non-deterministic behaviors of the data types. It was suggested to bound this non-determinism but that would result in a false verification. So it was mandatory to model data types using FOL. This resulted in a conclusion that CBMC is not the right tool for modeling checking Viper.