Automatic program analysis using Max-SMT

This thesis addresses the development of techniques to build fully-automatic tools for analyzing sequential programs written in imperative languages like C or C++. In order to do the reasoning about programs, the approach taken in this thesis follows the constraint-based method used in program analy... View More