ESBMC is a SMT-based context-bounded bounded model checker that aims to provide bit-precise verification of both ANSI-C and C++ programs. The presentation will briefly introduce the tool and then show the usage of libtooling as a frontend for the tool, including the problems we had during the development and what we hope for the future.
On the first half of the talk, I'll describe the tool and present some examples of its usage, including the verification of concurrent programs.
I'll then focus on the tool's new frontend, which generates the AST of the program using clang's libtooling and converts it to an internal format that's used for the verification. This second half of the presentation will be focused on the development of the C frontend and the yet to be C++ frontend, including how we had to adjust to the libtooling API.
The aim of the talk is to present the difficulties that we faced when moving away from our frontend to clang, including limitations we found during the development. I'll end the talk with what we hope for the future, as users of clang, which translates to easier access to some of clang's internals (specially the static analyser).
Speakers: Mikhail Gadelha