Home |
Personal Info |
Research |
Papers |
Teaching |
About |
Verification of C Programs Via Natural Semantics and Abstract Interpretation (Extended Abstract) (CV07)
[Page last updated on "agosto 29, 2007, 09:39:11".]Roberto Bagnara, Patricia M. Hill, Andrea Pescetti, and Enea Zaffanella
Abstract
We are witnessing a substantial lack of available tools able to verify the absence of relevant classes of run-time errors in code written in (reasonably rich fragments of) C and C++. This is despite the progress made in recent years in the fields of program analysis and verification, and despite the huge impact such tools could have on the quality of a good portion of our software universe. It is interesting to observe that, among the dozens of freely available software development tools, hardly any, by analyzing the program semantics, are able to certify the absence of important classes of run-time hazards such as, say, the widely known buffer overflows in C code. The reason is, of course, that C and C++ are complex languages and the techniques that can be used to dominate this complexity still do not reduce tool development to simple, manageable tasks. Our overall aim for this research is to investigate how known techniques based on natural semantics and abstract interpretation can be extended so as to conveniently formalize and implement a range of analysis and verification tools for modern imperative languages such as C and C++.
Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, and BibTeX entry.
enea.zaffanella@unipr.it
| Home | Personal Info | Research | Papers | Teaching | About