2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011) (2006)
Sept. 18, 2006 to Sept. 22, 2006
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASE.2006.26
Jooyong Lee , BRICS, University of Aarhus
Robby , Kansas State University
Xianghua Deng , 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.
Jooyong Lee, Robby , Xianghua Deng, "Bogor/Kiasan: A k-bounded Symbolic Execution for Checking Strong Heap Properties of Open Systems", 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), vol. 00, no. , pp. 157-166, 2006, doi:10.1109/ASE.2006.26