From Simulation to Verification (and Back)

In: Proceedings of the 2003 Winter Simulation Conference, New Orleans, LA, December 2003,

---

Authors

Harald Rueß and Leonardo de Moura

Abstract

Symbolic evaluation is the execution of software and software designs on inputs given as symbolic or explicit constants along with constraints on these inputs. Efficient symbolic evaluation is now feasible due to recent advances in efficient decision procedures and symbolic model checking. Symbolic evaluation can be applied to partially implemented descriptions and provides wider coverage and greater assurance than testing and traditional simulation alone. Unlike full formal verification, symbolic evaluation can be used in a partial manner that is more likely to succeed and yield some degree of assurance. Its main advantage is that it can be used within a smooth spectrum of analyses ranging from refutation based on explicit-state simulation to full-blown verification.

gzipped postscript or postscript

BibTeX Entry

@inproceedings{RuessDeMoura:WSC03,
        TITLE = {From Simulation to Verification (and Back)},
        AUTHOR = {Harald Rue{\ss} and Leonardo de Moura},
        BOOKTITLE = {WSC'03---Winter Simulation Conference},
        EDITOR = {S. Chick, P.J. Sanche, D. Ferrin, And D.J. Morrice (eds)},
        MONTH = {December},
        YEAR = {2003},
        ADDRESS = {New Orleans, LA}
}

---

Harald Ruess: ruess@csl.sri.com