Scalable and precise verification based on k-induction, symbolic execution and floating-point theory

In this thesis, we describe and evaluate approaches for the efficient reasoning of realworld C programs using either Bounded Model Checking (BMC) or symbolic execution. We present three main contributions. First, we describe three new technologies developed in a software verification tool to handle real-world programs: (1) a frontend based on a state-of-the-art compiler, (2) a new SMT backend with support for floating-point arithmetic and (3) an incremental bounded model checking algorithm. These technologies are implemented in ESBMC, an SMT-based bounded model checker for C programs; results show that these technologies enable the verification of a large number of programs. Second, we formalise and evaluate the bkind algorithm: a novel extension to the kinduction algorithm that improves its bug-finding capabilities by performing backward searches in the state space. The bkind algorithm is the main scientific contribution of this thesis. It was implemented in ESBMC, and we show that it uses fewer resources compared to the original k-induction algorithm to verify the same programs without impacting the results. Third, we evaluate the use of SMT solvers in a state-of-the-art symbolic execution tool to reduce the number of false bugs reported to the user. Our SMT-based refutation of false bugs algorithm was implemented in the clang static analyser and evaluated on a large set of real-world projects, including the MacOS kernel. Results show that our refutation algorithm cannot only remove false bugs but also speed up the analysis when bugs are refuted. The algorithm does not remove any true bug and only introduces a 1% slowdown if it is unable to remove any bugs