Verification of java programs using symbolic execution and invariant generation Export

@inproceedings{citeulike:1270643, abstract = {Software verification is recognized as an important and difficult problem. We present a novel framework, based on symbolic execution, for the automated verification of software. The framework uses annotations in the form of method specifications and loop invariants. We present a novel iterative...}, author = {Pasareanu, C. and Visser, W.}, booktitle = {Proceedings of the 11th International SPIN Workshop on Model Checking of Software}, citeulike-article-id = {1270643}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.5394}, keywords = {execution, symbolic}, posted-at = {2009-06-24 03:35:10}, priority = {5}, publisher = {Springer-Verlag}, series = {LNCS}, title = {Verification of java programs using symbolic execution and invariant generation}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.5394}, volume = {2989}, year = {2004} }

TY - CONF ID - citeulike:1270643 L3 - citeulike-article-id:1270643 N2 - Software verification is recognized as an important and difficult problem. We present a novel framework, based on symbolic execution, for the automated verification of software. The framework uses annotations in the form of method specifications and loop invariants. We present a novel iterative... SE - LNCS TI - Verification of java programs using symbolic execution and invariant generation PB - Springer-Verlag VL - 2989 T2 - Proceedings of the 11th International SPIN Workshop on Model Checking of Software KW - execution KW - symbolic AU - Pasareanu, C AU - Visser, W PY - 2004/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.3.5394 ER -