{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,29]],"date-time":"2023-05-29T09:11:04Z","timestamp":1685351464422},"reference-count":0,"publisher":"National Library of Serbia","issue":"4","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ComSIS","COMPUT SCI INF SYST","COMPUT SCI INFORM SY","COMPUTER SCI INFORM","COMSIS J"],"published-print":{"date-parts":[[2011]]},"abstract":"<jats:p>One important quantitative property of CPS (Cyber-Physical Systems) software\n   is its heap bound for which a precise analysis result needs to combine shape\n   analysis and numeric reasoning. In this paper, we present a framework for\n   statically finding symbolic heap bounds of CPS software. The basic idea is to\n   separate numeric reasoning from shape analysis by first constructing an ASTG\n   (Abstract State Transition Graph) and then extracting a pure numeric\n   representation which can be analyzed for the heap bounds. A quantitative\n   shape analysis method based on symbolic execution is defined in the framework\n   to generate the ASTG. The numeric representation is extracted based on\n   program slicing technique and inputted into an abstract interpretation tool\n   for computing the heap bounds. We take list manipulating programs as an\n   example to explain how to instantiate the framework for important data\n   structures and to exhibit its practicability. A novel list abstraction method\n   is also presented to support the instantiation of the framework.<\/jats:p>","DOI":"10.2298\/csis110302054l","type":"journal-article","created":{"date-parts":[[2011,10,13]],"date-time":"2011-10-13T06:59:22Z","timestamp":1318489162000},"page":"1251-1276","source":"Crossref","is-referenced-by-count":2,"title":["Quantitative analysis for symbolic heap bounds of CPS software"],"prefix":"10.2298","volume":"8","author":[{"given":"Renjian","family":"Li","sequence":"first","affiliation":[{"name":"National Laboratory for Parallel and Distributed Processing Changsha, China"}]},{"given":"Ji","family":"Wang","sequence":"additional","affiliation":[{"name":"National Laboratory for Parallel and Distributed Processing Changsha, China"}]},{"given":"Liqian","family":"Chen","sequence":"additional","affiliation":[{"name":"National Laboratory for Parallel and Distributed Processing Changsha, China"}]},{"given":"Wanwei","family":"Liu","sequence":"additional","affiliation":[{"name":"School of Computer, National University of Defense Technology Changsha, China"}]},{"given":"Dengping","family":"Wei","sequence":"additional","affiliation":[{"name":"School of Computer, National University of Defense Technology Changsha, China"}]}],"member":"1078","container-title":["Computer Science and Information Systems"],"original-title":[],"language":"en","deposited":{"date-parts":[[2023,5,29]],"date-time":"2023-05-29T08:30:27Z","timestamp":1685349027000},"score":1,"resource":{"primary":{"URL":"https:\/\/doiserbia.nb.rs\/Article.aspx?ID=1820-02141100054L"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"references-count":0,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2011]]}},"URL":"https:\/\/doi.org\/10.2298\/csis110302054l","relation":{},"ISSN":["1820-0214","2406-1018"],"issn-type":[{"value":"1820-0214","type":"print"},{"value":"2406-1018","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}