Paper Info
Title
Interval analysis of microcontroller code using abstract interpretation of hardware and software
Abstract
Static analysis is often performed on source code where intervals -- possibly the most widely used numeric abstract domain -- have successfully been used as a program abstraction for decades. Binary code on microcontroller platforms, however, is different from high-level code in that data is frequently altered using bitwise operations and the results of operations often depend on the hardware configuration. We describe a method that combines word- and bit-level interval analysis and integrates a hardware model by means of abstract interpretation in order to handle these peculiarities. Moreover, we show that this method proves powerful enough to derive invariants that could so far only be verified using computationally more expensive techniques such as model checking.
Year
DOI
Venue
2010
10.1145/1811212.1811216
SCOPES
Keywords
Field
DocType
binary code,model checking,abstract interpretation,hardware configuration,source code,bit-level interval analysis,numeric abstract domain,high-level code,microcontroller code,hardware model,static analysis,interval analysis,embedded system,embedded systems
Unreachable code,Static program analysis,Model checking,Computer science,Source code,Systematic code,Parallel computing,Redundant code,Code generation,Real-time computing,Computer hardware,Dead code
Conference
Citations 
PageRank 
References 
11
0.55
25
Authors
3
Name
Order
Citations
PageRank
Jörg Brauer121919.33
Thomas Noll232627.79
Bastian Schlich321417.98