{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,13]],"date-time":"2024-07-13T13:57:27Z","timestamp":1720879047077},"reference-count":9,"publisher":"World Scientific Pub Co Pte Lt","issue":"05","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Soft. Eng. Knowl. Eng."],"published-print":{"date-parts":[[2006,10]]},"abstract":"<jats:p> This paper presents a novel method, namely slicing execution, for model checking C programs with respect to temporal safety properties. The distinguished feature is that it shows a nice approach to the efficient reduction of state space by abstraction and symbolic representation. Slicing execution is founded on an over-approximated semantics of C programs by variable abstraction, and executes symbolically only the relevant statements under abstraction criteria to construct over-approximated finite models of programs, which may be model checked. The variable abstraction criterion begins with a proper initial set of program variables and may be iteratively refined according to spurious counterexamples generated during model checking. In general, the properties to be verified often involve only a few variables in practical programs. In these cases, significant state space reduction, as well as considerable improvement of the scalability, may be achieved. The presented method has been used to verify the initial handshake process of SSL protocol based on the C source code of openssl-0.9.6c. The experiment results confirm that slicing execution is not only practical but also effective. <\/jats:p>","DOI":"10.1142\/s0218194006002987","type":"journal-article","created":{"date-parts":[[2006,10,18]],"date-time":"2006-10-18T07:29:52Z","timestamp":1161156592000},"page":"747-768","source":"Crossref","is-referenced-by-count":3,"title":["SLICING EXECUTION FOR MODEL CHECKING C PROGRAMS"],"prefix":"10.1142","volume":"16","author":[{"given":"XIAODONG","family":"YI","sequence":"first","affiliation":[{"name":"National Laboratory for Parallel and Distributed Processing, Changsha, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"JI","family":"WANG","sequence":"additional","affiliation":[{"name":"National Laboratory for Parallel and Distributed Processing, Changsha, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"XUEJUN","family":"YANG","sequence":"additional","affiliation":[{"name":"National Laboratory for Parallel and Distributed Processing, Changsha, P. R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,21]]},"reference":[{"key":"rf15","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"rf16","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"rf18","doi-asserted-by":"publisher","DOI":"10.1007\/BF02948890"},{"key":"rf19","doi-asserted-by":"publisher","DOI":"10.1142\/S0218194001000487"},{"key":"rf25","first-page":"352","volume":"10","author":"Weiser M.","journal-title":"IEEE Trans. on Software Engineering (TSE)"},{"key":"rf26","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(88)90054-3"},{"key":"rf27","volume-title":"Computer-Aided Verification of Coordinating Processes \u2014 The Automata-Theoretic Approach","author":"Kurshan R. P.","year":"1994"},{"key":"rf29","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H"},{"key":"rf33","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exi028"}],"container-title":["International Journal of Software Engineering and Knowledge Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0218194006002987","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,6]],"date-time":"2019-08-06T21:48:50Z","timestamp":1565128130000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S0218194006002987"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10]]},"references-count":9,"journal-issue":{"issue":"05","published-online":{"date-parts":[[2011,11,21]]},"published-print":{"date-parts":[[2006,10]]}},"alternative-id":["10.1142\/S0218194006002987"],"URL":"https:\/\/doi.org\/10.1142\/s0218194006002987","relation":{},"ISSN":["0218-1940","1793-6403"],"issn-type":[{"value":"0218-1940","type":"print"},{"value":"1793-6403","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,10]]}}}