Home |
Personal Info |
Papers |
Teaching |
Links |
Verification of C Programs Via Natural Semantics and Abstract Interpretation (Extended Abstract)
Roberto Bagnara
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Patricia M. Hill
School of Computing
University of Leeds
Leeds, LS2 9JT
United Kingdom
Andrea Pescetti
Dipartimento di Matematica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Enea Zaffanella
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
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: HTML, PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, BibTeX entry.
[Page last updated on June 04, 2007, 16:20:54.]
bagnara@cs.unipr.it
Home | Personal | Papers | Teaching | Links