Geodesic
Quantitative Analysis for Symbolic Heap Bounds of CPS Software
Computer Science and Information Systems, Tome 8 (2011) no. 4.

Voir la notice de l'article provenant de la source Computer Science and Information Systems website

One important quantitative property of CPS (Cyber-Physical Systems) software is its heap bound for which a precise analysis result needs to combine shape analysis and numeric reasoning. In this paper, we present a framework for statically finding symbolic heap bounds of CPS software. The basic idea is to separate numeric reasoning from shape analysis by first constructing an ASTG (Abstract State Transition Graph) and then extracting a pure numeric representation which can be analyzed for the heap bounds. A quantitative shape analysis method based on symbolic execution is defined in the framework to generate the ASTG. The numeric representation is extracted based on program slicing technique and inputted into an abstract interpretation tool for computing the heap bounds. We take list manipulating programs as an example to explain how to instantiate the framework for important data structures and to exhibit its practicability. A novel list abstraction method is also presented to support the instantiation of the framework.
Keywords: CPS software, heap bounds, quantitative shape analysis, symbolic execution, program slicing 
@article{CSIS_2011_8_4_a16,
     author = {Renjian Li and Ji Wang and Liqian Chen and Wanwei Liu and Dengping Wei},
     title = {Quantitative {Analysis} for {Symbolic} {Heap} {Bounds} of {CPS} {Software}},
     journal = {Computer Science and Information Systems},
     publisher = {mathdoc},
     volume = {8},
     number = {4},
     year = {2011},
     url = {http://geodesic.mathdoc.fr/item/CSIS_2011_8_4_a16/}
}
TY  - JOUR
AU  - Renjian Li
AU  - Ji Wang
AU  - Liqian Chen
AU  - Wanwei Liu
AU  - Dengping Wei
TI  - Quantitative Analysis for Symbolic Heap Bounds of CPS Software
JO  - Computer Science and Information Systems
PY  - 2011
VL  - 8
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/CSIS_2011_8_4_a16/
ID  - CSIS_2011_8_4_a16
ER  - 
%0 Journal Article
%A Renjian Li
%A Ji Wang
%A Liqian Chen
%A Wanwei Liu
%A Dengping Wei
%T Quantitative Analysis for Symbolic Heap Bounds of CPS Software
%J Computer Science and Information Systems
%D 2011
%V 8
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/CSIS_2011_8_4_a16/
%F CSIS_2011_8_4_a16
Renjian Li; Ji Wang; Liqian Chen; Wanwei Liu; Dengping Wei. Quantitative Analysis for Symbolic Heap Bounds of CPS Software. Computer Science and Information Systems, Tome 8 (2011) no. 4. http://geodesic.mathdoc.fr/item/CSIS_2011_8_4_a16/