首页>
外文OA文献
>Formal Program Verification Using Symbolic Execution
【2h】
Formal Program Verification Using Symbolic Execution
展开▼
机译:使用符号执行的正式程序验证
展开▼
免费
页面导航
摘要
著录项
相似文献
相关主题
摘要
Symbolic execution provides a mechanism for formally proving programs correct. A notation is introduced which allows a concise presentation of rules of inference based on symbolic execution. Using this notation, rules of inference are developed to handle a number of language features, including loops and procedures with multiple exits. An attribute grammar is used to formally describe symbolic expression evaluation, and the treatment of function calls with side effects is shown to be straightforward. Because symbolic execution is related to program interpretation, it is an easy-to-comprehend, yet powerful technique. The rules of inference are useful in expressing the semantics of a language and form the basis of a mechanical verification condition generator.
展开▼