21st IEEE/ACM International Conference on Automated Software Engineering (ASE'06) (2006)
Sept. 18, 2006 to Sept. 22, 2006
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASE.2006.26
Xianghua Deng , Kansas State University
Jooyong Lee , BRICS, University of Aarhus
Robby , Kansas State University
This paper presents Kiasan, a bounded technique to reason about open systems based on a path sensitive, relatively sound and complete symbolic execution instead of the usual compositional reasoning through weakest precondition calculation that summarizes all execution paths. Kiasan is able to check strong heap properties, and it is fully automatic and flexible in terms of its cost and the guarantees it provides. It allows a user-adjustable mixed compositional/non-compositional reasoning and naturally produces error traces as fault evidence. We implemented Kiasan using the Bogor model checking framework and observed that its performance is comparable to ESC/Java on similar scales of problems and behavioral coverage, while providing the ability to check much stronger specifications.
J. Lee, Robby and X. Deng, "Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems," 21st IEEE/ACM International Conference on Automated Software Engineering (ASE'06)(ASE), Tokyo, Japan, 2006, pp. 157-166.