Formal static analysis of C programs.
Formal Methods have been used in the domain of software verification where the software is to be deployed in safety-critical environments. We adopted Abstract Interpretation based Formal Methods and several abstract domains were surveyed. Zonotope Abstract Domain(an abstract domain based on affine arithmetic) was found to be suitable for the current project. We carried out a thorough study of the literature regarding the same. Our aim was towards the modified implementation of Zonotope Abstract Domain for it to work in conjunction with other abstract domains, to build a complete numerical-analysis software for C programs.