|
Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Orient |
- Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs, April 2007.
Xianghua Deng, Robby, and John Hatcliff.
Technical Report, SAnToS-TR2007-3 (accepted at SEFM 2007).
pdf (extended version, last updated: June 24, 2007)
The extended version includes: (1) experiment data summaries for Kiasan (using the lazy/lazier/lazier# initialization algorithms), (2) swap's (lazy/lazier/lazier#) symbolic states, (3) expanded description of the case counting method (red-black tree, binary search tree, and AVL tree), and (4) Kiasan's (lazy/lazier/lazier#) formal semantics and relative soundness/completeness proofs.
Experiment Data: lazy initialization, lazier initialization, lazier# initialization
|
