DocumentCode :
402209
Title :
From simulation to verification (and back)
Author :
Rueb ; De Moura, Leonardo
Author_Institution :
Comput. Sci. Lab., SRI Int., Menlo Park, CA, USA
Volume :
1
fYear :
2003
fDate :
7-10 Dec. 2003
Firstpage :
888
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.
Keywords :
digital simulation; formal specification; formal verification; systems analysis; decision procedures; explicit constants; explicit-state simulation; formal verification; full-blown verification; partial use; program specification; refutation; software designs; software execution; symbolic constants; symbolic evaluation; symbolic model checking; Automatic testing; Circuit simulation; Data structures; Formal verification; Hardware; Logic; Power system modeling; Protocols; Safety; State-space methods;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Simulation Conference, 2003. Proceedings of the 2003 Winter
Print_ISBN :
0-7803-8131-9
Type :
conf
DOI :
10.1109/WSC.2003.1261508
Filename :
1261508
Link To Document :
بازگشت