Paper Info
Title
Symbolic and Abstract Interpretation for C/C++ Programs
Abstract
We present a construction technique for abstract interpretations which is generic in the choice of data abstractions. The technique is specialised on C/C++ code, internally represented by the GIMPLE control flow graph as generated by the gcc compiler. The generic interpreter handles program transitions in a symbolic way, while recording a history of symbolic memory valuations. An abstract interpreter is instantiated by selecting appropriate lattices for the data types under consideration. This selection induces an instance of the generic transition relation. All resulting abstract interpretations can handle pointer arithmetic, type casts, unions and the aliasing problems involved. It is illustrated how switching between abstractions can improve the efficiency of the verification process. The concepts described in this paper are implemented in the test automation and static analysis tool RT-Tester which is used for the verification of embedded systems in the fields of avionics, railways and automotive control.
Year
DOI
Venue
2008
10.1016/j.entcs.2008.06.045
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
generic transition relation,construction technique,data abstraction,abstract interpretation,automated testing,symbolic memory valuation,automotive control,static analysis,generic interpreter,gimple control flow graph,data type,galois connections,abstract interpreter,embedded system,control flow graph,static analysis tools
Pointer (computer programming),Programming language,Control flow graph,Computer science,Abstract interpretation,Static analysis,Automation,Compiler,Theoretical computer science,Interpreter,Data type
Journal
Volume
ISSN
Citations 
217,
Electronic Notes in Theoretical Computer Science
6
PageRank 
References 
Authors
0.46
8
2
Name
Order
Citations
PageRank
Helge Löding1453.14
Jan Peleska253248.74